proposition: Lemma Inhabited_Setminus : forall X Y:Ensemble U, Included U X Y -> ~ Included U Y X -> Inhabited U (Setminus U Y X).
proof: Proof. intros X Y I NI. elim (not_all_ex_not U (fun x:U => In U Y x -> In U X x) NI). intros x YX. apply Inhabited_intro with x. apply Setminus_intro. - apply not_imply_elim with (In U X x); trivial with sets. - auto with sets. Qed.
imports: Ensembles Constructive_sets Classical