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