We will prove ¬ paracompact_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.

Assume Hpara: paracompact_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.

We will prove False.

We prove the intermediate claim HHline: Hausdorff_space Sorgenfrey_line Sorgenfrey_topology.

An exact proof term for the current goal is Sorgenfrey_line_Hausdorff.

We prove the intermediate claim HHplane: Hausdorff_space (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology.

An exact proof term for the current goal is (ex17_11_product_Hausdorff Sorgenfrey_line Sorgenfrey_topology Sorgenfrey_line Sorgenfrey_topology HHline HHline).

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

An exact proof term for the current goal is (paracompact_Hausdorff_normal (setprod Sorgenfrey_line Sorgenfrey_line) Sorgenfrey_plane_topology Hpara HHplane).

We prove the intermediate claim Hnotnorm: ¬ 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 (Hnotnorm Hnorm).

∎