proposition: Lemma interior_maximal: forall U:Ensemble X, open U -> Included U S -> Included U interior.
proof: Proof. intros. red; intros. exists U; trivial. constructor; split; trivial. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)