Let X be given.
Assume Hwo: well_ordered_set X.
Assume Hso: simply_ordered_set X.
Assume H0X: 0 ∈ X.
We will prove {0} ∈ order_topology X.
We prove the intermediate claim HordX: ordinal X.
An exact proof term for the current goal is (well_ordered_set_is_ordinal X Hwo).
We prove the intermediate claim Hord1: ordinal 1.
An exact proof term for the current goal is (nat_p_ordinal 1 nat_1).
Apply (ordinal_trichotomy_or_impred X 1 HordX Hord1 ({0} ∈ order_topology X)) to the current goal.
Assume HXin1: X ∈ 1.
We will prove {0} ∈ order_topology X.
Apply FalseE to the current goal.
We prove the intermediate claim HXeq0: X = 0.
We prove the intermediate claim HXin0: X ∈ {0}.
rewrite the current goal using (eq_1_Sing0) (from right to left).
An exact proof term for the current goal is HXin1.
An exact proof term for the current goal is (SingE 0 X HXin0).
We prove the intermediate claim H0in0: 0 ∈ 0.
rewrite the current goal using HXeq0 (from right to left) at position 2.
An exact proof term for the current goal is H0X.
An exact proof term for the current goal is (EmptyE 0 H0in0).
Assume HXeq1: X = 1.
rewrite the current goal using HXeq1 (from left to right).
We prove the intermediate claim Htop1: topology_on 1 (order_topology 1).
rewrite the current goal using HXeq1 (from right to left).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
rewrite the current goal using (eq_1_Sing0) (from right to left).
An exact proof term for the current goal is (topology_has_X 1 (order_topology 1) Htop1).
Assume H1inX: 1 ∈ X.
An exact proof term for the current goal is (singleton0_open_in_order_topology_well_ordered X Hwo H1inX).
∎