proposition: Lemma interior_union: forall S T:Ensemble X, Included (Union (interior S) (interior T)) (interior (Union S T)).
proof: Proof. intros. apply interior_maximal. - apply open_union2; apply interior_open. - pose proof (interior_deflationary S). pose proof (interior_deflationary T). auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)