Let a and b be given.

Assume HaR: a ∈ R.

Assume HbR: b ∈ R.

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).

∎