Set X to be the term setprod 2 ω.

We prove the intermediate claim H1O: 1 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 1 nat_1).

We prove the intermediate claim HsX: (0,1) ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 1 In_0_2 H1O).

Set s to be the term (0,1).

Set U to be the term open_ray_lower X s.

We prove the intermediate claim HUpow: U ∈ 𝒫 X.

Apply PowerI X U to the current goal.

Let y be given.

Assume Hy: y ∈ U.

An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X y0 s) y Hy).

We prove the intermediate claim HUinB: U ∈ order_topology_basis X.

An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X s HsX).

We prove the intermediate claim HUopen: U ∈ order_topology X.

An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) U HUpow HUinB).

We will prove {(0,0)} ∈ order_topology X.

rewrite the current goal using (open_ray_lower_setprod_2_omega_01_eq_Sing00) (from right to left).

An exact proof term for the current goal is HUopen.

∎