Let X and a be given.
Assume Hso: simply_ordered_set X.
Assume HaX: a ∈ X.
We will prove {x ∈ X|order_rel X a x} ∈ order_topology X.
Set U to be the term open_ray_upper X a.
We prove the intermediate claim HUinB: U ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_upper_in_order_topology_basis X a HaX).
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.
∎