proposition: Lemma family_union_singleton (S : Ensemble T) : FamilyUnion (Singleton S) = S.
proof: Proof. now extensionality_ensembles; try econstructor. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)