Let U and x be given.
Assume HU: U ∈ R_standard_topology.
Assume HxU: x ∈ U.
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (SepE1 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim HUsubR: U ⊆ R.
An exact proof term for the current goal is (PowerE R U HUpow).
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (HUsubR x HxU).
We prove the intermediate claim HUprop: ∃I ∈ R_standard_basis, x ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_standard_basis, x0 ∈ b ∧ b ⊆ U0) U HU x HxU).
Apply HUprop to the current goal.
Let I be given.
Assume HIpair.
We prove the intermediate claim HIStd: I ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I ∈ R_standard_basis) (x ∈ I ∧ I ⊆ U) HIpair).
We prove the intermediate claim HIprop: x ∈ I ∧ I ⊆ U.
An exact proof term for the current goal is (andER (I ∈ R_standard_basis) (x ∈ I ∧ I ⊆ U) HIpair).
We prove the intermediate claim HxI: x ∈ I.
An exact proof term for the current goal is (andEL (x ∈ I) (I ⊆ U) HIprop).
We prove the intermediate claim HIsubU: I ⊆ U.
An exact proof term for the current goal is (andER (x ∈ I) (I ⊆ U) HIprop).
We prove the intermediate claim Hexa: ∃a ∈ R, I ∈ {open_interval a b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) I HIStd).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
Apply Hapair to the current goal.
Assume HaR: a ∈ R.
Assume HIfam: I ∈ {open_interval a b|b ∈ R}.
We prove the intermediate claim Hexb: ∃b ∈ R, I = open_interval a b.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0) I HIfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
Apply Hbpair to the current goal.
Assume HbR: b ∈ R.
Assume HIeq: I = open_interval a b.
We use a to witness the existential quantifier.
We use b to witness the existential quantifier.
We prove the intermediate claim HxIn: x ∈ open_interval a b.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HxI.
We prove the intermediate claim HxProp: Rlt a x ∧ Rlt x b.
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt a z ∧ Rlt z b) x HxIn).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaR.
An exact proof term for the current goal is HbR.
An exact proof term for the current goal is HxIn.
rewrite the current goal using HIeq (from right to left).
An exact proof term for the current goal is HIsubU.
An exact proof term for the current goal is (andEL (Rlt a x) (Rlt x b) HxProp).
An exact proof term for the current goal is (andER (Rlt a x) (Rlt x b) HxProp).
∎