proposition: Lemma Build_TopologicalSpace_from_closed_sets_closed: forall (F:Ensemble (point_set Build_TopologicalSpace_from_closed_sets)), closed F <-> closedP F.
proof: Proof. intros. unfold closed. simpl. rewrite Complement_Complement. split; trivial. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)