proposition: Lemma Hausdorff_ProductTopology2 {X Y : TopologicalSpace} : Hausdorff X -> Hausdorff Y -> Hausdorff (ProductTopology2 X Y).
proof: Proof. intros HX HY [x0 y0] [x1 y1] Hxy. specialize (HX x0 x1). specialize (HY y0 y1). destruct (classic (x0 = x1)) as [|Hx]. { subst. assert (y0 <> y1) as Hy by congruence. clear Hxy. specialize (HY Hy) as [U [V [HU [HV [HU0 [HV0 HUV]]]]]]. exists (EnsembleProduct Full_set U), (EnsembleProduct Full_set V). repeat split; auto using EnsembleProduct_open, open_full. simpl. rewrite EnsembleProduct_Intersection. rewrite Powerset_facts.Intersection_Full_set. rewrite HUV. apply EnsembleProduct_Empty_r. } clear Hxy. specialize (HX Hx) as [U [V [HU [HV [HU0 [HV0 HUV]]]]]]. exists (EnsembleProduct U Full_set), (EnsembleProduct V Full_set). repeat split; auto using EnsembleProduct_open, open_full. simpl. rewrite EnsembleProduct_Intersection. rewrite Powerset_facts.Intersection_Full_set. rewrite HUV. apply EnsembleProduct_Empty_l. Qed.
imports: Coq(FunctionalExtensionality) ZornsLemma(DependentTypeChoice EnsembleProduct FiniteIntersections)