Let a and b be given.
Assume Hab.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (RltE_left a b Hab).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (RltE_right a b Hab).
We prove the intermediate claim HbFam: open_interval a b ∈ {open_interval a b0|b0 ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a b0) b HbR).
We prove the intermediate claim HbStd: open_interval a b ∈ R_standard_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b0|b0 ∈ R}) a (open_interval a b) HaR HbFam).
We prove the intermediate claim HPow: open_interval a b ∈ 𝒫 R.
An exact proof term for the current goal is (PowerI R (open_interval a b) (open_interval_Subq_R a b)).
An exact proof term for the current goal is (generated_topology_contains_elem R R_standard_basis (open_interval a b) HPow HbStd).
∎