proposition: Lemma closed_family_intersection: forall {X:TopologicalSpace} (F:Family X), (forall S:Ensemble X, In F S -> closed S) -> closed (FamilyIntersection F).
proof: Proof. intros. unfold closed in H. red. rewrite Complement_FamilyIntersection. apply open_family_union. intros. destruct H0. subst. apply H, H0. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)