proposition: Lemma interior_idempotent : idempotent (@interior X).
proof: Proof. intro. apply Extensionality_Ensembles. split. - apply interior_deflationary. - red. intros. econstructor; [ | eassumption ]. constructor. split. + apply interior_open. + intro. exact id. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)