We will prove Hausdorff_space R R_lower_limit_topology.
We will prove topology_on R R_lower_limit_topology ∧ ∀x1 x2 : set, x1 ∈ R → x2 ∈ R → x1 ≠ x2 → ∃U V : set, U ∈ R_lower_limit_topology ∧ V ∈ R_lower_limit_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is R_lower_limit_topology_is_topology.
Let x1 and x2 be given.
Assume Hx1R: x1 ∈ R.
Assume Hx2R: x2 ∈ R.
Assume Hneq: x1 ≠ x2.
We will prove ∃U V : set, U ∈ R_lower_limit_topology ∧ V ∈ R_lower_limit_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hx1S: SNo x1.
An exact proof term for the current goal is (real_SNo x1 Hx1R).
We prove the intermediate claim Hx2S: SNo x2.
An exact proof term for the current goal is (real_SNo x2 Hx2R).
Apply (SNoLt_trichotomy_or_impred x1 x2 Hx1S Hx2S (∃U V : set, U ∈ R_lower_limit_topology ∧ V ∈ R_lower_limit_topology ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty)) to the current goal.
Assume Hlt: x1 < x2.
Set U to be the term halfopen_interval_left x1 x2.
Set b to be the term add_SNo x2 1.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (real_add_SNo x2 Hx2R 1 real_1).
Set V to be the term halfopen_interval_left x2 b.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x1 x2 Hx1R Hx2R).
We prove the intermediate claim HVopen: V ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x2 b Hx2R HbR).
We prove the intermediate claim Hx1U: x1 ∈ U.
We will prove x1 ∈ {x ∈ R|¬ (Rlt x x1) ∧ Rlt x x2}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx1R.
An exact proof term for the current goal is (andI (¬ (Rlt x1 x1)) (Rlt x1 x2) (not_Rlt_refl x1 Hx1R) (RltI x1 x2 Hx1R Hx2R Hlt)).
We prove the intermediate claim Hx2ltb: x2 < b.
We prove the intermediate claim H0lt1: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hx20: add_SNo x2 0 = x2.
An exact proof term for the current goal is (add_SNo_0R x2 Hx2S).
We prove the intermediate claim Hx2lt: add_SNo x2 0 < add_SNo x2 1.
An exact proof term for the current goal is (add_SNo_Lt2 x2 0 1 Hx2S SNo_0 SNo_1 H0lt1).
We will prove x2 < b.
rewrite the current goal using Hx20 (from right to left) at position 1.
An exact proof term for the current goal is Hx2lt.
We prove the intermediate claim Hx2V: x2 ∈ V.
We will prove x2 ∈ {x ∈ R|¬ (Rlt x x2) ∧ Rlt x b}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx2R.
An exact proof term for the current goal is (andI (¬ (Rlt x2 x2)) (Rlt x2 b) (not_Rlt_refl x2 Hx2R) (RltI x2 b Hx2R HbR Hx2ltb)).
We prove the intermediate claim HUVempty: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z Hz).
We prove the intermediate claim HzUprop: ¬ (Rlt z x1) ∧ Rlt z x2.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x x1) ∧ Rlt x x2) z HzU).
We prove the intermediate claim HzVprop: ¬ (Rlt z x2) ∧ Rlt z b.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x x2) ∧ Rlt x b) z HzV).
We prove the intermediate claim Hzltx2: Rlt z x2.
An exact proof term for the current goal is (andER (¬ (Rlt z x1)) (Rlt z x2) HzUprop).
We prove the intermediate claim Hznltx2: ¬ (Rlt z x2).
An exact proof term for the current goal is (andEL (¬ (Rlt z x2)) (Rlt z b) HzVprop).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hznltx2 Hzltx2).
Apply and5I to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is Hx1U.
An exact proof term for the current goal is Hx2V.
An exact proof term for the current goal is HUVempty.
Assume Heq: x1 = x2.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Heq).
Assume Hgt: x2 < x1.
Set U to be the term halfopen_interval_left x2 x1.
Set b to be the term add_SNo x1 1.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (real_add_SNo x1 Hx1R 1 real_1).
Set V to be the term halfopen_interval_left x1 b.
We use V to witness the existential quantifier.
We use U to witness the existential quantifier.
We prove the intermediate claim HVopen: V ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x1 b Hx1R HbR).
We prove the intermediate claim HUopen: U ∈ R_lower_limit_topology.
An exact proof term for the current goal is (halfopen_interval_left_in_R_lower_limit_topology x2 x1 Hx2R Hx1R).
We prove the intermediate claim Hx2U: x2 ∈ U.
We will prove x2 ∈ {x ∈ R|¬ (Rlt x x2) ∧ Rlt x x1}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx2R.
An exact proof term for the current goal is (andI (¬ (Rlt x2 x2)) (Rlt x2 x1) (not_Rlt_refl x2 Hx2R) (RltI x2 x1 Hx2R Hx1R Hgt)).
We prove the intermediate claim Hx1ltb: x1 < b.
We prove the intermediate claim H0lt1: 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We prove the intermediate claim Hx10: add_SNo x1 0 = x1.
An exact proof term for the current goal is (add_SNo_0R x1 Hx1S).
We prove the intermediate claim Hx1lt: add_SNo x1 0 < add_SNo x1 1.
An exact proof term for the current goal is (add_SNo_Lt2 x1 0 1 Hx1S SNo_0 SNo_1 H0lt1).
We will prove x1 < b.
rewrite the current goal using Hx10 (from right to left) at position 1.
An exact proof term for the current goal is Hx1lt.
We prove the intermediate claim Hx1V: x1 ∈ V.
We will prove x1 ∈ {x ∈ R|¬ (Rlt x x1) ∧ Rlt x b}.
Apply SepI to the current goal.
An exact proof term for the current goal is Hx1R.
An exact proof term for the current goal is (andI (¬ (Rlt x1 x1)) (Rlt x1 b) (not_Rlt_refl x1 Hx1R) (RltI x1 b Hx1R HbR Hx1ltb)).
We prove the intermediate claim HUVempty: V ∩ U = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ V ∩ U.
We will prove z ∈ Empty.
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE1 V U z Hz).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE2 V U z Hz).
We prove the intermediate claim HzVprop: ¬ (Rlt z x1) ∧ Rlt z b.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x x1) ∧ Rlt x b) z HzV).
We prove the intermediate claim HzUprop: ¬ (Rlt z x2) ∧ Rlt z x1.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ ¬ (Rlt x x2) ∧ Rlt x x1) z HzU).
We prove the intermediate claim Hzltx1: Rlt z x1.
An exact proof term for the current goal is (andER (¬ (Rlt z x2)) (Rlt z x1) HzUprop).
We prove the intermediate claim Hznltx1: ¬ (Rlt z x1).
An exact proof term for the current goal is (andEL (¬ (Rlt z x1)) (Rlt z b) HzVprop).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hznltx1 Hzltx1).
Apply and5I to the current goal.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is Hx1V.
An exact proof term for the current goal is Hx2U.
An exact proof term for the current goal is HUVempty.
∎