Let a be given.
Assume HaR: a ∈ R.
Set U to be the term {x ∈ R|¬ (Rlt x a)}.
We will prove U ∈ R_lower_limit_topology.
We will prove U ∈ generated_topology R R_lower_limit_basis.
We prove the intermediate claim HUsub: U ⊆ R.
Let x be given.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 a)) x HxU).
We prove the intermediate claim HUpow: U ∈ 𝒫 R.
An exact proof term for the current goal is (PowerI R U HUsub).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ R_lower_limit_basis, x0 ∈ b ∧ b ⊆ U.
Let x be given.
Assume HxU: x ∈ U.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 a)) x HxU).
We prove the intermediate claim HxNotLtA: ¬ (Rlt x a).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a)) x HxU).
We prove the intermediate claim Hax: Rle a x.
An exact proof term for the current goal is (RleI a x HaR HxR HxNotLtA).
We prove the intermediate claim Hx1R: (add_SNo x 1) ∈ R.
An exact proof term for the current goal is (real_add_SNo x HxR 1 real_1).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim H0S: SNo 0.
An exact proof term for the current goal is (real_SNo 0 real_0).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is (real_SNo 1 real_1).
We prove the intermediate claim Hx0lt: add_SNo x 0 < add_SNo x 1.
An exact proof term for the current goal is (add_SNo_Lt2 x 0 1 HxS H0S H1S SNoLt_0_1).
We prove the intermediate claim Hx0eq: add_SNo x 0 = x.
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hxlt: x < add_SNo x 1.
rewrite the current goal using Hx0eq (from right to left) at position 1.
An exact proof term for the current goal is Hx0lt.
We prove the intermediate claim HxRlt: Rlt x (add_SNo x 1).
An exact proof term for the current goal is (RltI x (add_SNo x 1) HxR Hx1R Hxlt).
We use (halfopen_interval_left x (add_SNo x 1)) to witness the existential quantifier.
Apply andI to the current goal.
We will prove halfopen_interval_left x (add_SNo x 1) ∈ R_lower_limit_basis.
Apply (famunionI R (λaa : set ⇒ {halfopen_interval_left aa bb|bb ∈ R}) x (halfopen_interval_left x (add_SNo x 1)) HxR) to the current goal.
We will prove halfopen_interval_left x (add_SNo x 1) ∈ {halfopen_interval_left x bb|bb ∈ R}.
An exact proof term for the current goal is (ReplI R (λbb : set ⇒ halfopen_interval_left x bb) (add_SNo x 1) Hx1R).
Apply andI to the current goal.
We will prove x ∈ halfopen_interval_left x (add_SNo x 1).
An exact proof term for the current goal is (halfopen_interval_left_leftmem x (add_SNo x 1) HxRlt).
We will prove halfopen_interval_left x (add_SNo x 1) ⊆ U.
Let t be given.
Assume HtB: t ∈ halfopen_interval_left x (add_SNo x 1).
We will prove t ∈ U.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z (add_SNo x 1)) t HtB).
We prove the intermediate claim HtProp: ¬ (Rlt t x) ∧ Rlt t (add_SNo x 1).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z x) ∧ Rlt z (add_SNo x 1)) t HtB).
We prove the intermediate claim HtNotLtX: ¬ (Rlt t x).
An exact proof term for the current goal is (andEL (¬ (Rlt t x)) (Rlt t (add_SNo x 1)) HtProp).
We will prove t ∈ {x0 ∈ R|¬ (Rlt x0 a)}.
Apply (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a)) t HtR) to the current goal.
Assume HtLtA: Rlt t a.
We prove the intermediate claim HtLtX: Rlt t x.
An exact proof term for the current goal is (Rlt_Rle_tra t a x HtLtA Hax).
An exact proof term for the current goal is (HtNotLtX HtLtX).
An exact proof term for the current goal is (SepI (𝒫 R) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ R_lower_limit_basis, x0 ∈ b ∧ b ⊆ U0) U HUpow HUprop).
∎