proposition: Lemma interior_intersection: forall S T:Ensemble X, interior (Intersection S T) = Intersection (interior S) (interior T).
proof: Proof. intros. apply Extensionality_Ensembles. split. - assert (Included (interior (Intersection S T)) (interior S)). { apply interior_increasing. auto with sets. } assert (Included (interior (Intersection S T)) (interior T)). { apply interior_increasing. auto with sets. } auto with sets. - apply interior_maximal. + apply open_intersection2; apply interior_open. + pose proof (interior_deflationary S). pose proof (interior_deflationary T). red. intros x H1. constructor; [ apply H | apply H0]; now destruct H1. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)