proposition: Lemma Build_TopologicalSpace_from_closure_operator_closure: forall S:Ensemble (point_set Build_TopologicalSpace_from_closure_operator), closure S = cl S.
proof: Proof. intros. apply Extensionality_Ensembles; split. - apply closure_minimal. + apply <- Build_TopologicalSpace_from_closed_sets_closed. apply cl_idempotent. + trivial. - replace (closure S) with (cl (closure S)). + apply cl_increasing. apply (closure_inflationary S). + pose proof (closure_closed S). apply -> Build_TopologicalSpace_from_closed_sets_closed in H. exact H. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)