proposition: Lemma Complement_Union {X : Type} (U V : Ensemble X) : Complement (Union U V) = Intersection (Complement U) (Complement V).
proof: Proof. unfold Complement. apply Extensionality_Ensembles; split; red; intros. - constructor; auto with sets. - subst. red; red; intro. destruct H. destruct H0; auto. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)