proposition: Lemma interior_fixes_open: open S -> interior = S.
proof: Proof. intros. apply Extensionality_Ensembles; split. - apply interior_deflationary. - red; intros. exists S; trivial. constructor. auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)