proposition: Lemma Build_TopologicalSpace_from_interior_operator_interior: forall S:Ensemble (point_set Build_TopologicalSpace_from_interior_operator), interior S = int S.
proof: Proof. intros. apply Extensionality_Ensembles; split. - red. intros. destruct H. destruct H. destruct H. simpl in *. eapply int_increasing; [ | erewrite H ]; eassumption. - red. intros. econstructor; [ | eassumption ]. constructor. split. + apply int_idempotent. + apply int_deflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)