proposition: Lemma family_intersection_singleton (S : Ensemble T) : FamilyIntersection (Singleton S) = S.
proof: Proof. apply Extensionality_Ensembles; split. - intros _ [x Hx]. apply Hx. constructor. - intros x Hx. constructor. intros U HU. destruct HU; assumption. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)