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