proposition: Lemma closed_finite_indexed_union: forall {X:TopologicalSpace} {A:Type} (F:IndexedFamily A X), FiniteT A -> (forall a:A, closed (F a)) -> closed (IndexedUnion F).
proof: Proof. intros. red. rewrite Complement_IndexedUnion. apply open_finite_indexed_intersection; trivial. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)