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