An exact proof term for the current goal is R_standard_basis_is_basis_local.

An exact proof term for the current goal is R_lower_limit_topology_is_topology.

Let U be given.

We prove the intermediate claim Hexa: ∃a0 ∈ R, U ∈ {open_interval a0 b0|b0 ∈ R}.

An exact proof term for the current goal is (famunionE R (λa1 : set ⇒ {open_interval a1 b1|b1 ∈ R}) U HU).

Apply Hexa to the current goal.

Let a0 be given.

Assume Ha0pair.

We prove the intermediate claim Ha0R: a0 ∈ R.

An exact proof term for the current goal is (andEL (a0 ∈ R) (U ∈ {open_interval a0 b0|b0 ∈ R}) Ha0pair).

We prove the intermediate claim HUfam: U ∈ {open_interval a0 b0|b0 ∈ R}.

An exact proof term for the current goal is (andER (a0 ∈ R) (U ∈ {open_interval a0 b0|b0 ∈ R}) Ha0pair).

We prove the intermediate claim Hexb: ∃b0 ∈ R, U = open_interval a0 b0.

An exact proof term for the current goal is (ReplE R (λb1 : set ⇒ open_interval a0 b1) U HUfam).

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0R: b0 ∈ R.

An exact proof term for the current goal is (andEL (b0 ∈ R) (U = open_interval a0 b0) Hb0pair).

We prove the intermediate claim HUeq: U = open_interval a0 b0.

An exact proof term for the current goal is (andER (b0 ∈ R) (U = open_interval a0 b0) Hb0pair).

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

An exact proof term for the current goal is (open_interval_in_R_lower_limit_topology a0 b0 Ha0R Hb0R).