Let X and b be given.
Assume Hso: simply_ordered_set X.
Assume HbX: b ∈ X.
We will prove {x ∈ X|order_rel X x b} ∈ order_topology X.
Set U to be the term open_ray_lower X b.
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 b HbX).
We prove the intermediate claim HBasis: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
We prove the intermediate claim HUinT: U ∈ generated_topology X (order_topology_basis X).
An exact proof term for the current goal is (basis_in_generated X (order_topology_basis X) U HBasis HUinB).
An exact proof term for the current goal is HUinT.
∎