Let A be given.
Assume HA: A ⊆ R.
Assume Hconn: connected_space A (subspace_topology R R_standard_topology A).
Let x, y and z be given.
Assume Hx: x ∈ A.
Assume Hy: y ∈ A.
Assume Hz: z ∈ R.
Assume Hbetw: Rlt x z ∧ Rlt z y ∨ Rlt y z ∧ Rlt z x.
We will prove z ∈ A.
Apply (xm (z ∈ A)) to the current goal.
Assume HzA: z ∈ A.
An exact proof term for the current goal is HzA.
Assume HznotA: z ∉ A.
Set U to be the term {t ∈ A|Rlt t z}.
Set V to be the term {t ∈ A|Rlt z t}.
We prove the intermediate claim Hnosep: ¬ (∃U0 V0 : set, U0 ∈ subspace_topology R R_standard_topology A ∧ V0 ∈ subspace_topology R R_standard_topology A ∧ separation_of A U0 V0).
An exact proof term for the current goal is (connected_space_no_separation A (subspace_topology R R_standard_topology A) Hconn).
We prove the intermediate claim HUinTy: U ∈ subspace_topology R R_standard_topology A.
Set L to be the term {t ∈ R|Rlt t z}.
We prove the intermediate claim HLopen: L ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology z Hz).
We prove the intermediate claim HUeq: U = L ∩ A.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ U.
We will prove t ∈ L ∩ A.
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt t0 z) t Ht).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HA t HtA).
We prove the intermediate claim Htlt: Rlt t z.
An exact proof term for the current goal is (SepE2 A (λt0 : set ⇒ Rlt t0 z) t Ht).
We prove the intermediate claim HtL: t ∈ L.
An exact proof term for the current goal is (SepI R (λt0 : set ⇒ Rlt t0 z) t HtR Htlt).
An exact proof term for the current goal is (binintersectI L A t HtL HtA).
Let t be given.
Assume Ht: t ∈ L ∩ A.
We will prove t ∈ U.
We prove the intermediate claim HtL: t ∈ L.
An exact proof term for the current goal is (binintersectE1 L A t Ht).
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (binintersectE2 L A t Ht).
We prove the intermediate claim Htlt: Rlt t z.
An exact proof term for the current goal is (SepE2 R (λt0 : set ⇒ Rlt t0 z) t HtL).
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt t0 z) t HtA Htlt).
We prove the intermediate claim HUpow: U ∈ 𝒫 A.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ U.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt t0 z) t Ht).
We prove the intermediate claim Hex: ∃W ∈ R_standard_topology, U = W ∩ A.
We use L to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HLopen.
An exact proof term for the current goal is HUeq.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ R_standard_topology, U0 = W ∩ A) U HUpow Hex).
We prove the intermediate claim HVinTy: V ∈ subspace_topology R R_standard_topology A.
Set Rray to be the term {t ∈ R|Rlt z t}.
We prove the intermediate claim HRopen: Rray ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology z Hz).
We prove the intermediate claim HVeql: V = Rray ∩ A.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ V.
We will prove t ∈ Rray ∩ A.
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt z t0) t Ht).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HA t HtA).
We prove the intermediate claim Htlt: Rlt z t.
An exact proof term for the current goal is (SepE2 A (λt0 : set ⇒ Rlt z t0) t Ht).
We prove the intermediate claim HtRray: t ∈ Rray.
An exact proof term for the current goal is (SepI R (λt0 : set ⇒ Rlt z t0) t HtR Htlt).
An exact proof term for the current goal is (binintersectI Rray A t HtRray HtA).
Let t be given.
Assume Ht: t ∈ Rray ∩ A.
We will prove t ∈ V.
We prove the intermediate claim HtRray: t ∈ Rray.
An exact proof term for the current goal is (binintersectE1 Rray A t Ht).
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (binintersectE2 Rray A t Ht).
We prove the intermediate claim Htlt: Rlt z t.
An exact proof term for the current goal is (SepE2 R (λt0 : set ⇒ Rlt z t0) t HtRray).
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt z t0) t HtA Htlt).
We prove the intermediate claim HVpow: V ∈ 𝒫 A.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ V.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt z t0) t Ht).
We prove the intermediate claim Hex: ∃W ∈ R_standard_topology, V = W ∩ A.
We use Rray to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HRopen.
An exact proof term for the current goal is HVeql.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ R_standard_topology, U0 = W ∩ A) V HVpow Hex).
We prove the intermediate claim HsepUV: separation_of A U V.
We prove the intermediate claim HUsubA: U ⊆ A.
Let t be given.
Assume Ht: t ∈ U.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt t0 z) t Ht).
We prove the intermediate claim HVsubA: V ⊆ A.
Let t be given.
Assume Ht: t ∈ V.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt z t0) t Ht).
We prove the intermediate claim HUpowA: U ∈ 𝒫 A.
An exact proof term for the current goal is (PowerI A U HUsubA).
We prove the intermediate claim HVpowA: V ∈ 𝒫 A.
An exact proof term for the current goal is (PowerI A V HVsubA).
We prove the intermediate claim Hdisj: U ∩ V = Empty.
Apply Empty_eq to the current goal.
Let t be given.
Assume Ht: t ∈ U ∩ V.
Apply (binintersectE U V t Ht) to the current goal.
Assume HtU: t ∈ U.
Assume HtV: t ∈ V.
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt t0 z) t HtU).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HA t HtA).
We prove the intermediate claim Hlt1: Rlt t z.
An exact proof term for the current goal is (SepE2 A (λt0 : set ⇒ Rlt t0 z) t HtU).
We prove the intermediate claim Hlt2: Rlt z t.
An exact proof term for the current goal is (SepE2 A (λt0 : set ⇒ Rlt z t0) t HtV).
We prove the intermediate claim Htt: Rlt t t.
An exact proof term for the current goal is (Rlt_tra t z t Hlt1 Hlt2).
Apply FalseE to the current goal.
An exact proof term for the current goal is ((not_Rlt_refl t HtR) Htt).
We prove the intermediate claim HUne: U ≠ Empty.
Apply (xm (Rlt x z ∧ Rlt z y)) to the current goal.
Assume Hxzzy: Rlt x z ∧ Rlt z y.
We prove the intermediate claim Hxz: Rlt x z.
An exact proof term for the current goal is (andEL (Rlt x z) (Rlt z y) Hxzzy).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt t0 z) x Hx Hxz).
An exact proof term for the current goal is (elem_implies_nonempty U x HxU).
Assume Hnot.
We prove the intermediate claim Hyz: Rlt y z.
Apply Hbetw to the current goal.
Assume Hxzzy: Rlt x z ∧ Rlt z y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot Hxzzy).
Assume Hyzzx: Rlt y z ∧ Rlt z x.
An exact proof term for the current goal is (andEL (Rlt y z) (Rlt z x) Hyzzx).
We prove the intermediate claim HyU: y ∈ U.
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt t0 z) y Hy Hyz).
An exact proof term for the current goal is (elem_implies_nonempty U y HyU).
We prove the intermediate claim HVne: V ≠ Empty.
Apply (xm (Rlt x z ∧ Rlt z y)) to the current goal.
Assume Hxzzy: Rlt x z ∧ Rlt z y.
We prove the intermediate claim Hzy: Rlt z y.
An exact proof term for the current goal is (andER (Rlt x z) (Rlt z y) Hxzzy).
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt z t0) y Hy Hzy).
An exact proof term for the current goal is (elem_implies_nonempty V y HyV).
Assume Hnot.
We prove the intermediate claim Hzx: Rlt z x.
Apply Hbetw to the current goal.
Assume Hxzzy: Rlt x z ∧ Rlt z y.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnot Hxzzy).
Assume Hyzzx: Rlt y z ∧ Rlt z x.
An exact proof term for the current goal is (andER (Rlt y z) (Rlt z x) Hyzzx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (SepI A (λt0 : set ⇒ Rlt z t0) x Hx Hzx).
An exact proof term for the current goal is (elem_implies_nonempty V x HxV).
We prove the intermediate claim Hunion: U ∪ V = A.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ U ∪ V.
We will prove t ∈ A.
Apply (binunionE U V t Ht) to the current goal.
Assume HtU.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt t0 z) t HtU).
Assume HtV.
An exact proof term for the current goal is (SepE1 A (λt0 : set ⇒ Rlt z t0) t HtV).
Let t be given.
Assume HtA: t ∈ A.
We will prove t ∈ U ∪ V.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HA t HtA).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HzS: SNo z.
An exact proof term for the current goal is (real_SNo z Hz).
Apply (SNoLt_trichotomy_or_impred t z HtS HzS (t ∈ U ∪ V)) to the current goal.
Assume Hlt: t < z.
We prove the intermediate claim Htlt: Rlt t z.
An exact proof term for the current goal is (RltI t z HtR Hz Hlt).
An exact proof term for the current goal is (binunionI1 U V t (SepI A (λt0 : set ⇒ Rlt t0 z) t HtA Htlt)).
Assume Heq: t = z.
We prove the intermediate claim HzA: z ∈ A.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HtA.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HznotA HzA).
Assume Hlt: z < t.
We prove the intermediate claim Hzt: Rlt z t.
An exact proof term for the current goal is (RltI z t Hz HtR Hlt).
An exact proof term for the current goal is (binunionI2 U V t (SepI A (λt0 : set ⇒ Rlt z t0) t HtA Hzt)).
We will prove (((((U ∈ 𝒫 A ∧ V ∈ 𝒫 A) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) ∧ U ∪ V = A).
Apply andI to the current goal.
We will prove ((((U ∈ 𝒫 A ∧ V ∈ 𝒫 A) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
Apply andI to the current goal.
We will prove (((U ∈ 𝒫 A ∧ V ∈ 𝒫 A) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
Apply andI to the current goal.
We will prove (U ∈ 𝒫 A ∧ V ∈ 𝒫 A) ∧ U ∩ V = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUpowA.
An exact proof term for the current goal is HVpowA.
An exact proof term for the current goal is Hdisj.
An exact proof term for the current goal is HUne.
An exact proof term for the current goal is HVne.
An exact proof term for the current goal is Hunion.
Apply FalseE to the current goal.
Apply Hnosep to the current goal.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUinTy.
An exact proof term for the current goal is HVinTy.
An exact proof term for the current goal is HsepUV.
∎