proposition: Lemma Setminus_Intersection {X : Type} (U V : Ensemble X) : Setminus U V = Intersection U (Complement V).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - destruct H. split; assumption. - destruct H. split; assumption. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)