Let U be given.

Assume HU: U ∈ metric_topology R R_bounded_metric.

Set B to be the term famunion R (λx0 : set ⇒ {open_ball R R_bounded_metric x0 r0|r0 ∈ R, Rlt 0 r0}).

We prove the intermediate claim Htop: 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 HBsub: ∀b0 ∈ B, b0 ∈ R_standard_topology.

Let b0 be given.

Assume Hb0: b0 ∈ B.

Apply (famunionE_impred R (λx0 : set ⇒ {open_ball R R_bounded_metric x0 r0|r0 ∈ R, Rlt 0 r0}) b0 Hb0 (b0 ∈ R_standard_topology)) to the current goal.

Let c0 be given.

Assume Hc0R: c0 ∈ R.

Assume Hb0In: b0 ∈ {open_ball R R_bounded_metric c0 r0|r0 ∈ R, Rlt 0 r0}.

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball R R_bounded_metric c0 r0) b0 Hb0In (b0 ∈ R_standard_topology)) to the current goal.

Let r0 be given.

Assume Hr0R: r0 ∈ R.

Assume Hr0pos: Rlt 0 r0.

Assume Hb0eq: b0 = open_ball R R_bounded_metric c0 r0.

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

An exact proof term for the current goal is (open_ball_R_bounded_metric_in_R_standard_topology_early c0 r0 Hc0R Hr0R Hr0pos).

We prove the intermediate claim Hsub: generated_topology R B ⊆ R_standard_topology.

An exact proof term for the current goal is (generated_topology_finer_weak R B R_standard_topology Htop HBsub).

An exact proof term for the current goal is (Hsub U HU).

Let U be given.

Assume HU: U ∈ R_standard_topology.

We will prove U ∈ metric_topology R R_bounded_metric.

We prove the intermediate claim Htop: topology_on R (metric_topology R R_bounded_metric).

An exact proof term for the current goal is (metric_topology_is_topology R R_bounded_metric R_bounded_metric_is_metric_on_early).

We prove the intermediate claim HBsub: ∀b0 ∈ R_standard_basis, b0 ∈ metric_topology R R_bounded_metric.

Let b0 be given.

Assume Hb0: b0 ∈ R_standard_basis.

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

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

Apply Hexa to the current goal.

Let a0 be given.

Assume Hapair: a0 ∈ R ∧ b0 ∈ {open_interval a0 bb|bb ∈ R}.

We prove the intermediate claim Ha0R: a0 ∈ R.

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

We prove the intermediate claim Hb0Fam: b0 ∈ {open_interval a0 bb|bb ∈ R}.

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

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

An exact proof term for the current goal is (ReplE R (λbb0 : set ⇒ open_interval a0 bb0) b0 Hb0Fam).

Apply Hexb to the current goal.

Let bb be given.

Assume Hbpair: bb ∈ R ∧ b0 = open_interval a0 bb.

We prove the intermediate claim HbbR: bb ∈ R.

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

We prove the intermediate claim Hb0eq: b0 = open_interval a0 bb.

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

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

An exact proof term for the current goal is (open_interval_in_metric_topology_R_bounded_metric_early a0 bb Ha0R HbbR).

We prove the intermediate claim Hsub: generated_topology R R_standard_basis ⊆ metric_topology R R_bounded_metric.

An exact proof term for the current goal is (generated_topology_finer_weak R R_standard_basis (metric_topology R R_bounded_metric) Htop HBsub).

We prove the intermediate claim HUgen: U ∈ generated_topology R R_standard_basis.

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

An exact proof term for the current goal is HU.

An exact proof term for the current goal is (Hsub U HUgen).