Let X be given.
Assume Hso: simply_ordered_set X.
We will prove regular_space X (order_topology X).
We will prove one_point_sets_closed X (order_topology X) ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X (order_topology X) F → x ∉ F → ∃U V : set, U ∈ order_topology X ∧ V ∈ order_topology X ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We prove the intermediate claim HH: Hausdorff_space X (order_topology X).
An exact proof term for the current goal is (ex17_10_order_topology_Hausdorff X Hso).
We will prove one_point_sets_closed X (order_topology X).
We will prove topology_on X (order_topology X) ∧ ∀x : set, x ∈ X → closed_in X (order_topology X) {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (Hausdorff_space_topology X (order_topology X) HH).
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X (order_topology X) x HH HxX).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X (order_topology X) F.
Assume HxnotF: x ∉ F.
An exact proof term for the current goal is (order_topology_regular_sep X x F Hso HxX HFcl HxnotF).
∎