Let U be given.

Assume HU: U ∈ order_topology R.

We will prove U ∈ R_standard_topology.

We prove the intermediate claim HdefOrd: order_topology R = generated_topology R (order_topology_basis R).

Use reflexivity.

We prove the intermediate claim HdefStd: R_standard_topology = generated_topology R R_standard_basis.

An exact proof term for the current goal is R_standard_topology_def_eq.

We prove the intermediate claim HUgen: U ∈ generated_topology R (order_topology_basis R).

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

An exact proof term for the current goal is HU.

We prove the intermediate claim HUpow: U ∈ 𝒫 R.

An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ order_topology_basis R, x ∈ b ∧ b ⊆ U0) U HUgen).

We prove the intermediate claim HUloc: ∀x ∈ U, ∃b ∈ order_topology_basis R, x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ order_topology_basis R, x ∈ b ∧ b ⊆ U0) U HUgen).

We prove the intermediate claim HUlocStd: ∀x ∈ U, ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U.

Let x0 be given.

Assume Hx0U: x0 ∈ U.

Apply (HUloc x0 Hx0U) to the current goal.

Let b0 be given.

Assume Hb0core.

We prove the intermediate claim Hb0B: b0 ∈ order_topology_basis R.

An exact proof term for the current goal is (andEL (b0 ∈ order_topology_basis R) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0core).

We prove the intermediate claim Hrest: x0 ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ order_topology_basis R) (x0 ∈ b0 ∧ b0 ⊆ U) Hb0core).

We prove the intermediate claim Hx0b0: x0 ∈ b0.

An exact proof term for the current goal is (andEL (x0 ∈ b0) (b0 ⊆ U) Hrest).

We prove the intermediate claim Hb0subU: b0 ⊆ U.

An exact proof term for the current goal is (andER (x0 ∈ b0) (b0 ⊆ U) Hrest).

We prove the intermediate claim HexI: ∃I ∈ R_standard_basis, x0 ∈ I ∧ I ⊆ b0.

An exact proof term for the current goal is (order_topology_basis_R_refines_standard_basis b0 Hb0B x0 Hx0b0).

Apply HexI to the current goal.

Let I be given.

Assume HIcore.

Apply HIcore to the current goal.

Assume HIbasis: I ∈ R_standard_basis.

Assume HIrest: x0 ∈ I ∧ I ⊆ b0.

We prove the intermediate claim Hx0I: x0 ∈ I.

An exact proof term for the current goal is (andEL (x0 ∈ I) (I ⊆ b0) HIrest).

We prove the intermediate claim HIsubb0: I ⊆ b0.

An exact proof term for the current goal is (andER (x0 ∈ I) (I ⊆ b0) HIrest).

We use I to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HIbasis.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0I.

An exact proof term for the current goal is (Subq_tra I b0 U HIsubb0 Hb0subU).

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

An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U0) U HUpow HUlocStd).

Let U be given.

Assume HU: U ∈ R_standard_topology.

We will prove U ∈ order_topology R.

We prove the intermediate claim HdefStd: R_standard_topology = generated_topology R R_standard_basis.

An exact proof term for the current goal is R_standard_topology_def_eq.

We prove the intermediate claim HdefOrd: order_topology R = generated_topology R (order_topology_basis R).

Use reflexivity.

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

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

An exact proof term for the current goal is HU.

We prove the intermediate claim HUpow: U ∈ 𝒫 R.

An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U0) U HUgen).

We prove the intermediate claim HUloc: ∀x ∈ U, ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U0) U HUgen).

We prove the intermediate claim HUlocOrd: ∀x ∈ U, ∃b ∈ order_topology_basis R, x ∈ b ∧ b ⊆ U.

Let x0 be given.

Assume Hx0U: x0 ∈ U.

Apply (HUloc x0 Hx0U) to the current goal.

Let I be given.

Assume HIcore.

Apply HIcore to the current goal.

Assume HIbasis: I ∈ R_standard_basis.

Assume HIrest: x0 ∈ I ∧ I ⊆ U.

We prove the intermediate claim Hx0I: x0 ∈ I.

An exact proof term for the current goal is (andEL (x0 ∈ I) (I ⊆ U) HIrest).

We prove the intermediate claim HIsubU: I ⊆ U.

An exact proof term for the current goal is (andER (x0 ∈ I) (I ⊆ U) HIrest).

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

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

Apply Hexa to the current goal.

Let a0 be given.

Assume Ha0core.

Apply Ha0core to the current goal.

Assume Ha0R: a0 ∈ R.

Assume HIaFam: I ∈ {open_interval a0 bb|bb ∈ R}.

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

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

Apply Hexb to the current goal.

Let b0 be given.

Assume Hb0core.

Apply Hb0core to the current goal.

Assume Hb0R: b0 ∈ R.

Assume HIeq: I = open_interval a0 b0.

Set b to be the term open_interval a0 b0.

We prove the intermediate claim HbBasis: b ∈ order_topology_basis R.

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

We prove the intermediate claim Hx0b: x0 ∈ b.

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

An exact proof term for the current goal is Hx0I.

We prove the intermediate claim HbsubU: b ⊆ U.

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

An exact proof term for the current goal is HIsubU.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbBasis.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0b.

An exact proof term for the current goal is HbsubU.

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

An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x ∈ U0, ∃b ∈ order_topology_basis R, x ∈ b ∧ b ⊆ U0) U HUpow HUlocOrd).