proposition: Lemma open_indexed_union: forall {X:TopologicalSpace} {A:Type} (F:IndexedFamily A X), (forall a:A, open (F a)) -> open (IndexedUnion F).
proof: Proof. intros. rewrite indexed_to_family_union. apply open_family_union. intros. destruct H0. rewrite H1; apply H. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)