proposition: Lemma open_empty: forall X:TopologicalSpace, open (@Empty_set X).
proof: Proof. intros. rewrite <- empty_family_union. apply open_family_union. intros. destruct H. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)