proposition: Lemma closed_intersection2: forall {X:TopologicalSpace} (F G:Ensemble X), closed F -> closed G -> closed (Intersection F G).
proof: Proof. intros. red in H, H0. red. rewrite Complement_Intersection. apply open_union2; trivial. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)