proposition: Lemma open_finite_indexed_intersection: forall {X:TopologicalSpace} {A:Type} (F:IndexedFamily A X), FiniteT A -> (forall a:A, open (F a)) -> open (IndexedIntersection F).
proof: Proof. intros X A F HA HF. apply open_finite_intersections. apply finite_indexed_intersection_is_finite_intersection; assumption. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)