proposition: Lemma intersection_as_family_intersection (U V : Ensemble T) : Intersection U V = FamilyIntersection (Couple U V).
proof: Proof. apply Extensionality_Ensembles; split; red. - intros _ [x Hx0 Hx1]. constructor. intros _ [|]; assumption. - intros _ [x Hx]. split; apply Hx; clear Hx; constructor. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)