proposition: Lemma interior_closure_idempotent: idempotent (fun S => interior (@closure X S)).
proof: Proof. intro. extensionality_ensembles; destruct H. - eapply interior_maximal; try eassumption. eapply Inclusion_is_transitive; [ eassumption | ]. red. intros. destruct H2 as [? H2]. apply H2. constructor. split. + apply closure_closed. + apply interior_deflationary. - econstructor; [ | eassumption ]. constructor. split; try eassumption. eapply Inclusion_is_transitive. + eapply interior_maximal; eassumption. + apply closure_inflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)