Let a be given.
Assume HaR.
Set U to be the term {x ∈ R|Rlt a x}.
We will prove U ∈ R_standard_topology.
We prove the intermediate claim HUinPow: U ∈ 𝒫 R.
Apply PowerI to the current goal.
Let x be given.
Assume Hx.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0) x Hx).
We prove the intermediate claim HUprop: ∀x ∈ U, ∃b ∈ R_standard_basis, x ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0) x HxU).
We prove the intermediate claim Hax: Rlt a x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0) x HxU).
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Set e0 to be the term eps_ 0.
We prove the intermediate claim He0SNoS: e0 ∈ SNoS_ ω.
An exact proof term for the current goal is (SNo_eps_SNoS_omega 0 H0omega).
We prove the intermediate claim He0R: e0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real e0 He0SNoS).
We prove the intermediate claim HbR: add_SNo x e0 ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR e0 He0R).
Set b to be the term open_interval a (add_SNo x e0).
We prove the intermediate claim HbStd: b ∈ R_standard_basis.
We prove the intermediate claim HbFam: b ∈ {open_interval a b0|b0 ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a b0) (add_SNo x e0) HbR).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b0|b0 ∈ R}) a b HaR HbFam).
We prove the intermediate claim Hxinb: x ∈ b.
We prove the intermediate claim Hxlt: x < add_SNo x e0.
An exact proof term for the current goal is (add_SNo_eps_Lt x (real_SNo x HxR) 0 H0omega).
We prove the intermediate claim Hxxe0: Rlt x (add_SNo x e0).
An exact proof term for the current goal is (RltI x (add_SNo x e0) HxR HbR Hxlt).
We prove the intermediate claim Hpropb: Rlt a x ∧ Rlt x (add_SNo x e0).
Apply andI to the current goal.
An exact proof term for the current goal is Hax.
An exact proof term for the current goal is Hxxe0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 (add_SNo x e0)) x HxR Hpropb).
We prove the intermediate claim HbSubU: b ⊆ U.
Let y be given.
Assume Hyb.
We prove the intermediate claim HyR: y ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 (add_SNo x e0)) y Hyb).
We prove the intermediate claim Hyprop: Rlt a y ∧ Rlt y (add_SNo x e0).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 (add_SNo x e0)) y Hyb).
We prove the intermediate claim Hay: Rlt a y.
An exact proof term for the current goal is (andEL (Rlt a y) (Rlt y (add_SNo x e0)) Hyprop).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt a x0) y HyR Hay).
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbStd.
Apply andI to the current goal.
An exact proof term for the current goal is Hxinb.
An exact proof term for the current goal is HbSubU.
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b0 ∈ R_standard_basis, x0 ∈ b0 ∧ b0 ⊆ U0) U HUinPow HUprop).
∎