proposition: Lemma interior_increasing: forall S T:Ensemble X, Included S T -> Included (interior S) (interior T).
proof: Proof. intros. apply interior_maximal. - apply interior_open. - assert (Included (interior S) S) by apply interior_deflationary. auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)