proposition: Lemma EnsembleProduct_open {X Y : TopologicalSpace} (U : Ensemble X) (V : Ensemble Y) : open U -> open V -> @open (@ProductTopology2 X Y) (EnsembleProduct U V).
proof: Proof. intros. apply ProductTopology2_basis_is_basis. constructor; assumption. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)