Let a and b be given.
Assume HaR: a ∈ R.
Assume HbR: b ∈ R.
We will prove halfopen_interval_left a b ∈ R_lower_limit_topology.
We prove the intermediate claim HbFam: halfopen_interval_left a b ∈ {halfopen_interval_left a bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left a bb) b HbR).
We prove the intermediate claim HbBasis: halfopen_interval_left a b ∈ R_lower_limit_basis.
An exact proof term for the current goal is (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) a (halfopen_interval_left a b) HaR HbFam).
An exact proof term for the current goal is (generated_topology_contains_basis R R_lower_limit_basis R_lower_limit_basis_is_basis_local (halfopen_interval_left a b) HbBasis).
∎