proposition: Lemma not_included_empty_Inhabited : forall A:Ensemble U, ~ Included U A (Empty_set U) -> Inhabited U A.
proof: Proof. intros A NI. elim (not_all_ex_not U (fun x:U => ~ In U A x)). - intros x H; apply Inhabited_intro with x. apply NNPP; auto with sets. - red; intro. apply NI; red. intros x H'; elim (H x); trivial with sets. Qed.
imports: Ensembles Constructive_sets Classical