proposition: Lemma closed_complement_open: forall {X:TopologicalSpace} (U:Ensemble X), closed (Ensembles.Complement U) -> open U.
proof: Proof. intros. red in H. rewrite Complement_Complement in H. assumption. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)