Let A be given.

We prove the intermediate claim HtopA: topology_on A (subspace_topology R R_standard_topology A).

We prove the intermediate claim HAin: A ∈ subspace_topology R R_standard_topology A.

An exact proof term for the current goal is (topology_has_X A (subspace_topology R R_standard_topology A) HtopA).

We prove the intermediate claim HexV: ∃V ∈ R_standard_topology, A = V ∩ A.

An exact proof term for the current goal is (SepE2 (𝒫 A) (λU0 : set ⇒ ∃V ∈ R_standard_topology, U0 = V ∩ A) A HAin).

Apply HexV to the current goal.

Let V be given.

Assume HVpair.

We prove the intermediate claim HV: V ∈ R_standard_topology.

An exact proof term for the current goal is (andEL (V ∈ R_standard_topology) (A = V ∩ A) HVpair).

We prove the intermediate claim HAeq: A = V ∩ A.

An exact proof term for the current goal is (andER (V ∈ R_standard_topology) (A = V ∩ A) HVpair).

We prove the intermediate claim HT: topology_on R R_standard_topology.

An exact proof term for the current goal is R_standard_topology_is_topology_local.

We prove the intermediate claim HVsubR: V ⊆ R.

An exact proof term for the current goal is (topology_elem_subset R R_standard_topology V HT HV).

We prove the intermediate claim HA: A ⊆ R.

Let x be given.

Assume HxA: x ∈ A.

We prove the intermediate claim HxVA: x ∈ V ∩ A.

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

An exact proof term for the current goal is HxA.

We prove the intermediate claim HxV: x ∈ V.

An exact proof term for the current goal is (binintersectE1 V A x HxVA).

An exact proof term for the current goal is (HVsubR x HxV).

An exact proof term for the current goal is (Heine_Borel_closed_bounded A HA Hcomp).

∎