proposition: Lemma open_union2: forall {X:TopologicalSpace} (U V:Ensemble X), open U -> open V -> open (Union U V).
proof: Proof. intros. rewrite union_as_family_union. apply open_family_union. intros. destruct H1; trivial. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)