Let a be given.

Assume HaR.

rewrite the current goal using (R_minus_singleton_eq_rays_union a HaR) (from left to right).

Apply (binunion_in_R_standard_topology {x ∈ R|Rlt x a} {x ∈ R|Rlt a x}) to the current goal.

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

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

∎