Let a and b be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

We prove the intermediate claim HTl: topology_on R R_lower_limit_topology.

An exact proof term for the current goal is R_lower_limit_topology_is_topology.

Set L to be the term {x ∈ R|Rlt x a}.

Set Rr to be the term {x ∈ R|¬ (Rlt x b)}.

We prove the intermediate claim HLstd: L ∈ R_standard_topology.

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

We prove the intermediate claim Hf: R_standard_topology ⊆ R_lower_limit_topology.

An exact proof term for the current goal is R_lower_limit_finer_than_R_standard.

We prove the intermediate claim HL: L ∈ R_lower_limit_topology.

An exact proof term for the current goal is (Hf L HLstd).

We prove the intermediate claim HRr: Rr ∈ R_lower_limit_topology.

An exact proof term for the current goal is (right_closed_ray_in_R_lower_limit_topology b HbR).

We prove the intermediate claim Hunion: L ∪ Rr ∈ R_lower_limit_topology.

An exact proof term for the current goal is (topology_binunion_closed R R_lower_limit_topology L Rr HTl HL HRr).

We prove the intermediate claim Heq: R ∖ halfopen_interval_left a b = L ∪ Rr.

An exact proof term for the current goal is (halfopen_interval_left_complement_eq_rays a b HaR HbR).

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

An exact proof term for the current goal is Hunion.

∎