Let X be given.

Assume Hwo: well_ordered_set X.

Assume H1X: 1 ∈ X.

We will prove {0} ∈ order_topology X.

rewrite the current goal using (open_ray_lower_well_ordered_1_eq_singleton0 X Hwo H1X) (from right to left).

An exact proof term for the current goal is (open_ray_lower_in_order_topology X 1 H1X).

∎