Apply andI to the current goal.

We prove the intermediate claim HnormS: normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology.

An exact proof term for the current goal is (andEL (normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology) (¬ normal_space (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology)) (SOmega_SbarOmega_not_normal)).

We prove the intermediate claim Hnorm1: normal_space S_Omega SOmega_topology.

An exact proof term for the current goal is (andEL (normal_space S_Omega SOmega_topology) (normal_space Sbar_Omega SbarOmega_topology) HnormS).

We prove the intermediate claim Hnorm2: normal_space Sbar_Omega SbarOmega_topology.

An exact proof term for the current goal is (andER (normal_space S_Omega SOmega_topology) (normal_space Sbar_Omega SbarOmega_topology) HnormS).

We prove the intermediate claim Hcr1: completely_regular_space S_Omega SOmega_topology.

An exact proof term for the current goal is (normal_space_implies_completely_regular S_Omega SOmega_topology Hnorm1).

We prove the intermediate claim Hcr2: completely_regular_space Sbar_Omega SbarOmega_topology.

An exact proof term for the current goal is (normal_space_implies_completely_regular Sbar_Omega SbarOmega_topology Hnorm2).

An exact proof term for the current goal is (completely_regular_product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology Hcr1 Hcr2).

We prove the intermediate claim Hnot: ¬ normal_space (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology).

An exact proof term for the current goal is (andER (normal_space S_Omega SOmega_topology ∧ normal_space Sbar_Omega SbarOmega_topology) (¬ normal_space (setprod S_Omega Sbar_Omega) (product_topology S_Omega SOmega_topology Sbar_Omega SbarOmega_topology)) (SOmega_SbarOmega_not_normal)).

An exact proof term for the current goal is Hnot.

∎