Let X and b be given.
Assume HbX: b ∈ X.
We will prove open_ray_lower X b ∈ order_topology X.
Set U to be the term open_ray_lower X b.
We prove the intermediate claim HUpow: U ∈ 𝒫 X.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X x0 b) x HxU).
We prove the intermediate claim HUbasis: U ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X b HbX).
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) U HUpow HUbasis).
∎