Let a be given.

Assume HaR: a ∈ R.

We will prove open_ray_upper R a ∈ R_standard_topology.

rewrite the current goal using standard_topology_is_order_topology (from right to left).

An exact proof term for the current goal is (open_ray_upper_in_order_topology R a HaR).

∎