Let x be given.

We will prove countable_basis_at Sorgenfrey_line Sorgenfrey_topology x.

Set Tx to be the term R_lower_limit_topology.

Set Bx to be the term Repl ω (λN0 : set ⇒ halfopen_interval_left x (add_SNo x (eps_ N0))).

We will prove topology_on Sorgenfrey_line Tx ∧ x ∈ Sorgenfrey_line ∧ ∃B : set, B ⊆ Tx ∧ countable_set B ∧ (∀b : set, b ∈ B → x ∈ b) ∧ (∀U : set, U ∈ Tx → x ∈ U → ∃b : set, b ∈ B ∧ b ⊆ U).

Apply andI to the current goal.

An exact proof term for the current goal is R_lower_limit_topology_is_topology.

An exact proof term for the current goal is HxR.

We use Bx to witness the existential quantifier.

Apply andI to the current goal.

Let b be given.

Assume Hb: b ∈ Bx.

We will prove b ∈ Tx.

We prove the intermediate claim HexN: ∃N ∈ ω, b = halfopen_interval_left x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (ReplE ω (λN0 : set ⇒ halfopen_interval_left x (add_SNo x (eps_ N0))) b Hb).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (b = halfopen_interval_left x (add_SNo x (eps_ N))) HNpair).

We prove the intermediate claim HbEq: b = halfopen_interval_left x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (andER (N ∈ ω) (b = halfopen_interval_left x (add_SNo x (eps_ N))) HNpair).

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 HepsR: eps_ N ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).

We prove the intermediate claim HepsS: SNo (eps_ N).

An exact proof term for the current goal is (real_SNo (eps_ N) HepsR).

We prove the intermediate claim HxplusR: add_SNo x (eps_ N) ∈ R.

An exact proof term for the current goal is (real_add_SNo x HxR (eps_ N) HepsR).

We prove the intermediate claim HxplusS: SNo (add_SNo x (eps_ N)).

An exact proof term for the current goal is (real_SNo (add_SNo x (eps_ N)) HxplusR).

We prove the intermediate claim HxltS: x < add_SNo x (eps_ N).

An exact proof term for the current goal is (add_SNo_eps_Lt x HxS N HNomega).

We prove the intermediate claim Hxlt: Rlt x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (RltI x (add_SNo x (eps_ N)) HxR HxplusR HxltS).

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

An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x (add_SNo x (eps_ N)) HxR HxplusR).

We prove the intermediate claim HomegaCount: countable_set ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

An exact proof term for the current goal is (countable_image ω HomegaCount (λN0 : set ⇒ halfopen_interval_left x (add_SNo x (eps_ N0)))).

Let b be given.

Assume Hb: b ∈ Bx.

We will prove x ∈ b.

We prove the intermediate claim HexN: ∃N ∈ ω, b = halfopen_interval_left x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (ReplE ω (λN0 : set ⇒ halfopen_interval_left x (add_SNo x (eps_ N0))) b Hb).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (b = halfopen_interval_left x (add_SNo x (eps_ N))) HNpair).

We prove the intermediate claim HbEq: b = halfopen_interval_left x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (andER (N ∈ ω) (b = halfopen_interval_left x (add_SNo x (eps_ N))) HNpair).

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 HepsR: eps_ N ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).

We prove the intermediate claim HxplusR: add_SNo x (eps_ N) ∈ R.

An exact proof term for the current goal is (real_add_SNo x HxR (eps_ N) HepsR).

We prove the intermediate claim HxltS: x < add_SNo x (eps_ N).

An exact proof term for the current goal is (add_SNo_eps_Lt x HxS N HNomega).

We prove the intermediate claim Hxlt: Rlt x (add_SNo x (eps_ N)).

An exact proof term for the current goal is (RltI x (add_SNo x (eps_ N)) HxR HxplusR HxltS).

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

An exact proof term for the current goal is (halfopen_interval_left_leftmem x (add_SNo x (eps_ N)) Hxlt).

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We will prove ∃b : set, b ∈ Bx ∧ b ⊆ U.

We prove the intermediate claim HTdef: Tx = generated_topology R R_lower_limit_basis.

Use reflexivity.

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

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

An exact proof term for the current goal is HU.

We prove the intermediate claim Hloc: ∀y0 ∈ U, ∃b0 ∈ R_lower_limit_basis, y0 ∈ b0 ∧ b0 ⊆ U.

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

We prove the intermediate claim Hexb0: ∃b0 ∈ R_lower_limit_basis, x ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (Hloc x HxU).

Apply Hexb0 to the current goal.

Let b0 be given.

Assume Hb0pair.

We prove the intermediate claim Hb0B: b0 ∈ R_lower_limit_basis.

An exact proof term for the current goal is (andEL (b0 ∈ R_lower_limit_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hb0prop: x ∈ b0 ∧ b0 ⊆ U.

An exact proof term for the current goal is (andER (b0 ∈ R_lower_limit_basis) (x ∈ b0 ∧ b0 ⊆ U) Hb0pair).

We prove the intermediate claim Hxb0: x ∈ b0.

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

We prove the intermediate claim Hb0subU: b0 ⊆ U.

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

We prove the intermediate claim Hexa: ∃a ∈ R, b0 ∈ {halfopen_interval_left a b|b ∈ R}.

An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {halfopen_interval_left a0 b|b ∈ R}) b0 Hb0B).

Apply Hexa to the current goal.

Let a be given.

Assume Hapair.

Apply Hapair to the current goal.

Assume HaR: a ∈ R.

Assume Hb0fam: b0 ∈ {halfopen_interval_left a b|b ∈ R}.

We prove the intermediate claim Hexb: ∃b ∈ R, b0 = halfopen_interval_left a b.

An exact proof term for the current goal is (ReplE R (λb1 : set ⇒ halfopen_interval_left a b1) b0 Hb0fam).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpair.

Apply Hbpair to the current goal.

Assume HbR: b ∈ R.

Assume Hb0eq: b0 = halfopen_interval_left a b.

We prove the intermediate claim HxIn: x ∈ halfopen_interval_left a b.

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

An exact proof term for the current goal is Hxb0.

We prove the intermediate claim HxProp: ¬ (Rlt x a) ∧ Rlt x b.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) x HxIn).

We prove the intermediate claim Hnltxa: ¬ (Rlt x a).

An exact proof term for the current goal is (andEL (¬ (Rlt x a)) (Rlt x b) HxProp).

We prove the intermediate claim Hxltb: Rlt x b.

An exact proof term for the current goal is (andER (¬ (Rlt x a)) (Rlt x b) HxProp).

We prove the intermediate claim Hax: Rle a x.

An exact proof term for the current goal is (RleI a x HaR HxR Hnltxa).

We prove the intermediate claim Hab: Rlt a b.

An exact proof term for the current goal is (Rle_Rlt_tra a x b Hax Hxltb).

Set d to be the term add_SNo b (minus_SNo x).

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 HbS: SNo b.

An exact proof term for the current goal is (real_SNo b HbR).

We prove the intermediate claim HmxS: SNo (minus_SNo x).

An exact proof term for the current goal is (SNo_minus_SNo x HxS).

We prove the intermediate claim HdR: d ∈ R.

An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo x) (real_minus_SNo x HxR)).

We prove the intermediate claim HdS: SNo d.

An exact proof term for the current goal is (real_SNo d HdR).

We prove the intermediate claim HxltbS: x < b.

An exact proof term for the current goal is (RltE_lt x b Hxltb).

We prove the intermediate claim HdposS: 0 < d.

An exact proof term for the current goal is (SNoLt_minus_pos x b HxS HbS HxltbS).

We prove the intermediate claim Hdpos: Rlt 0 d.

An exact proof term for the current goal is (RltI 0 d real_0 HdR HdposS).

We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < d.

An exact proof term for the current goal is (exists_eps_lt_pos d HdR Hdpos).

Apply HexN to the current goal.

Let N be given.

Assume HNpair.

We prove the intermediate claim HNomega: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < d) HNpair).

We prove the intermediate claim HepsLtD: eps_ N < d.

An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < d) HNpair).

Set b1 to be the term add_SNo x (eps_ N).

Set V to be the term halfopen_interval_left x b1.

We use V to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HVeq: V = halfopen_interval_left x (add_SNo x (eps_ N)).

Use reflexivity.

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

An exact proof term for the current goal is (ReplI ω (λN0 : set ⇒ halfopen_interval_left x (add_SNo x (eps_ N0))) N HNomega).

Let z be given.

Assume HzV: z ∈ V.

We will prove z ∈ U.

We prove the intermediate claim HepsR: eps_ N ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).

We prove the intermediate claim HepsS: SNo (eps_ N).

An exact proof term for the current goal is (real_SNo (eps_ N) HepsR).

We prove the intermediate claim Hb1R: b1 ∈ R.

An exact proof term for the current goal is (real_add_SNo x HxR (eps_ N) HepsR).

We prove the intermediate claim Hb1S: SNo b1.

An exact proof term for the current goal is (real_SNo b1 Hb1R).

We prove the intermediate claim Hxltb1S: x < b1.

An exact proof term for the current goal is (add_SNo_eps_Lt x HxS N HNomega).

We prove the intermediate claim Hxltb1: Rlt x b1.

An exact proof term for the current goal is (RltI x b1 HxR Hb1R Hxltb1S).

We prove the intermediate claim HxplusLt: add_SNo x (eps_ N) < add_SNo x d.

An exact proof term for the current goal is (add_SNo_Lt2 x (eps_ N) d HxS HepsS HdS HepsLtD).

We prove the intermediate claim HxdEq: add_SNo x d = b.

rewrite the current goal using (add_SNo_assoc x b (minus_SNo x) HxS HbS HmxS) (from left to right).

rewrite the current goal using (add_SNo_com x b HxS HbS) (from left to right).

rewrite the current goal using (add_SNo_assoc b x (minus_SNo x) HbS HxS HmxS) (from right to left).

rewrite the current goal using (add_SNo_minus_SNo_rinv x HxS) (from left to right).

An exact proof term for the current goal is (add_SNo_0R b HbS).

We prove the intermediate claim Hb1ltbS: b1 < b.

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

An exact proof term for the current goal is HxplusLt.

We prove the intermediate claim Hb1ltb: Rlt b1 b.

An exact proof term for the current goal is (RltI b1 b Hb1R HbR Hb1ltbS).

We prove the intermediate claim HzR: z ∈ R.

An exact proof term for the current goal is (SepE1 R (λz0 : set ⇒ ¬ (Rlt z0 x) ∧ Rlt z0 b1) z HzV).

We prove the intermediate claim HzProp: ¬ (Rlt z x) ∧ Rlt z b1.

An exact proof term for the current goal is (SepE2 R (λz0 : set ⇒ ¬ (Rlt z0 x) ∧ Rlt z0 b1) z HzV).

We prove the intermediate claim Hnltzx: ¬ (Rlt z x).

An exact proof term for the current goal is (andEL (¬ (Rlt z x)) (Rlt z b1) HzProp).

We prove the intermediate claim Hzltb1: Rlt z b1.

An exact proof term for the current goal is (andER (¬ (Rlt z x)) (Rlt z b1) HzProp).

We prove the intermediate claim Hxz: Rle x z.

An exact proof term for the current goal is (RleI x z HxR HzR Hnltzx).

We prove the intermediate claim Haz: Rle a z.

An exact proof term for the current goal is (Rle_tra a x z Hax Hxz).

We prove the intermediate claim Hnltza: ¬ (Rlt z a).

An exact proof term for the current goal is (RleE_nlt a z Haz).

We prove the intermediate claim Hzltb: Rlt z b.

An exact proof term for the current goal is (Rlt_tra z b1 b Hzltb1 Hb1ltb).

We prove the intermediate claim HzInb0: z ∈ halfopen_interval_left a b.

An exact proof term for the current goal is (SepI R (λz0 : set ⇒ ¬ (Rlt z0 a) ∧ Rlt z0 b) z HzR (andI (¬ (Rlt z a)) (Rlt z b) Hnltza Hzltb)).

We prove the intermediate claim HzInU: z ∈ U.

We prove the intermediate claim HzInb0': z ∈ b0.

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

An exact proof term for the current goal is HzInb0.

An exact proof term for the current goal is (Hb0subU z HzInb0').

An exact proof term for the current goal is HzInU.