proposition: Lemma closed_indexed_intersection: forall {X:TopologicalSpace} {A:Type} (F:IndexedFamily A X), (forall a:A, closed (F a)) -> closed (IndexedIntersection F).
proof: Proof. intros. rewrite indexed_to_family_intersection. apply closed_family_intersection. intros. destruct H0. rewrite H1; trivial. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)