Set X to be the term setprod 2 ω.
Set Tx to be the term order_topology X.
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is simply_ordered_set_setprod_2_omega.
We prove the intermediate claim HH: Hausdorff_space X Tx.
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
We will prove one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_one_point_sets_closed X Tx HH).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxnotF: x ∉ F.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply (xm (x = (1,0))) to the current goal.
Assume Hx10: x = (1,0).
Set U to be the term X ∖ F.
Set V to be the term F.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply and5I to the current goal.
We prove the intermediate claim HUopen_in: open_in X Tx U.
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFcl).
An exact proof term for the current goal is (open_in_elem X Tx U HUopen_in).
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).
We prove the intermediate claim Hnot10F: (1,0) ∉ F.
rewrite the current goal using Hx10 (from right to left).
An exact proof term for the current goal is HxnotF.
An exact proof term for the current goal is (open_in_order_topology_setprod_2_omega_if_not_10 F HFsubX Hnot10F).
An exact proof term for the current goal is (setminusI X F x HxX HxnotF).
An exact proof term for the current goal is (Subq_ref F).
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ V.
We will prove y ∈ Empty.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U V y Hy).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE2 U V y Hy).
We prove the intermediate claim HynotF: y ∉ F.
An exact proof term for the current goal is (setminusE2 X F y HyU).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HynotF HyV).
An exact proof term for the current goal is (Subq_Empty (U ∩ V)).
Assume Hxneq10: ¬ (x = (1,0)).
Set U to be the term {x}.
Set V to be the term X ∖ {x}.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is (singleton_setprod_2_omega_open_if_neq_10 x HxX Hxneq10).
We prove the intermediate claim Hxcl: closed_in X Tx {x}.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
We prove the intermediate claim HVopen_in: open_in X Tx V.
An exact proof term for the current goal is (open_of_closed_complement X Tx {x} Hxcl).
An exact proof term for the current goal is (open_in_elem X Tx V HVopen_in).
An exact proof term for the current goal is (SingI x).
Let y be given.
Assume HyF: y ∈ F.
We will prove y ∈ V.
Apply setminusI X {x} y to the current goal.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl y HyF).
Assume HySing: y ∈ {x}.
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y HySing).
Apply HxnotF to the current goal.
rewrite the current goal using HyEq (from right to left).
An exact proof term for the current goal is HyF.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ U ∩ V.
We will prove y ∈ Empty.
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (binintersectE1 U V y Hy).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (binintersectE2 U V y Hy).
We prove the intermediate claim HyEq: y = x.
An exact proof term for the current goal is (SingE x y HyU).
We prove the intermediate claim Hynot: y ∉ {x}.
An exact proof term for the current goal is (setminusE2 X {x} y HyV).
Apply FalseE to the current goal.
Apply Hynot to the current goal.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is (SingI x).
An exact proof term for the current goal is (Subq_Empty (U ∩ V)).
∎