We will prove completely_regular_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology ∧ ¬ normal_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.

Apply andI to the current goal.

We prove the intermediate claim HcrS: completely_regular_space Sorgenfrey_line Sorgenfrey_topology.

An exact proof term for the current goal is Sorgenfrey_line_completely_regular.

An exact proof term for the current goal is (completely_regular_product_topology Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology HcrS HcrS).

We prove the intermediate claim Hnot: ¬ normal_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.

An exact proof term for the current goal is (andER (regular_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology) (¬ normal_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology) (Sorgenfrey_plane_not_normal)).

An exact proof term for the current goal is Hnot.

∎