proposition: Lemma intersection_family_union : forall (S:Ensemble X) (F:Ensemble (Ensemble X)), In F S -> Intersection S (FamilyUnion F) = S.
proof: Proof. intros. extensionality_ensembles; trivial. constructor; trivial. econstructor; eassumption. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)