proposition: Lemma closed_union2: forall {X:TopologicalSpace} (F G:Ensemble X), closed F -> closed G -> closed (Union F G).
proof: Proof. intros. red in H, H0. red. rewrite Complement_Union. apply open_intersection2; assumption. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)