Let X and Tx be given.
Assume Hlin: linear_continuum X Tx.
We will prove locally_connected X Tx.
We prove the intermediate claim Hleft: (((simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y)) ∧ (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y)).
An exact proof term for the current goal is (andEL (((simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y)) ∧ (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y)) (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a : set, a ∈ A → order_rel X a upper ∨ a = upper) → ∃lub : set, lub ∈ X ∧ (∀a : set, a ∈ A → order_rel X a lub ∨ a = lub) ∧ (∀bound : set, bound ∈ X → (∀a : set, a ∈ A → order_rel X a bound ∨ a = bound) → order_rel X lub bound ∨ lub = bound)) Hlin).
We prove the intermediate claim HABC: ((simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y)).
An exact proof term for the current goal is (andEL ((simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y)) (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) Hleft).
We prove the intermediate claim HAB: simply_ordered_set X ∧ Tx = order_topology X.
An exact proof term for the current goal is (andEL (simply_ordered_set X ∧ Tx = order_topology X) (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y) HABC).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is (andEL (simply_ordered_set X) (Tx = order_topology X) HAB).
We prove the intermediate claim HTxeq: Tx = order_topology X.
An exact proof term for the current goal is (andER (simply_ordered_set X) (Tx = order_topology X) HAB).
We prove the intermediate claim Hlin0: linear_continuum X (order_topology X).
rewrite the current goal using HTxeq (from right to left).
An exact proof term for the current goal is Hlin.
rewrite the current goal using HTxeq (from left to right).
We will prove locally_connected X (order_topology X).
We prove the intermediate claim Hdef: locally_connected X (order_topology X) = (topology_on X (order_topology X) ∧ ∀x : set, x ∈ X → ∀U : set, U ∈ order_topology X → x ∈ U → ∃V : set, V ∈ order_topology X ∧ x ∈ V ∧ V ⊆ U ∧ connected_space V (subspace_topology X (order_topology X) V)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
Let x be given.
Assume HxX: x ∈ X.
Let U be given.
Assume HUopen: U ∈ order_topology X.
Assume HxU: x ∈ U.
We prove the intermediate claim Hexb: ∃b ∈ order_topology_basis X, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (order_topology_local_basis_elem X U x Hso HUopen HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB: b ∈ order_topology_basis X.
An exact proof term for the current goal is (andEL (b ∈ order_topology_basis X) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hbdata: x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (b ∈ order_topology_basis X) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate claim Hxb: x ∈ b.
An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbdata).
We prove the intermediate claim HbsubU: b ⊆ U.
An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbdata).
We use b to witness the existential quantifier.
We will prove b ∈ order_topology X ∧ x ∈ b ∧ b ⊆ U ∧ connected_space b (subspace_topology X (order_topology X) b).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HBasis: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
An exact proof term for the current goal is (basis_in_generated X (order_topology_basis X) b HBasis HbB).
An exact proof term for the current goal is Hxb.
An exact proof term for the current goal is HbsubU.
We prove the intermediate claim Hcases: (∃a ∈ X, ∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) ∨ (∃d ∈ X, b = {t ∈ X|order_rel X t d}) ∨ (∃a ∈ X, b = {t ∈ X|order_rel X a t}) ∨ b = X.
An exact proof term for the current goal is (order_topology_basis_cases X b HbB).
Apply Hcases to the current goal.
Assume H123: ((∃a ∈ X, ∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) ∨ (∃d ∈ X, b = {t ∈ X|order_rel X t d})) ∨ (∃a ∈ X, b = {t ∈ X|order_rel X a t}).
Apply H123 to the current goal.
Assume H12: (∃a ∈ X, ∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) ∨ (∃d ∈ X, b = {t ∈ X|order_rel X t d}).
Apply H12 to the current goal.
Assume Hinter: ∃a ∈ X, ∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}.
Apply Hinter to the current goal.
Let a be given.
Assume HaCore.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (andEL (a ∈ X) (∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) HaCore).
We prove the intermediate claim HdEx: ∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}.
An exact proof term for the current goal is (andER (a ∈ X) (∃d ∈ X, b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) HaCore).
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
We prove the intermediate claim HdX: d ∈ X.
An exact proof term for the current goal is (andEL (d ∈ X) (b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) HdCore).
We prove the intermediate claim HbEq: b = {t ∈ X|order_rel X a t ∧ order_rel X t d}.
An exact proof term for the current goal is (andER (d ∈ X) (b = {t ∈ X|order_rel X a t ∧ order_rel X t d}) HdCore).
We prove the intermediate claim HbEqI: b = order_interval X a d.
rewrite the current goal using HbEq (from left to right).
Use reflexivity.
rewrite the current goal using HbEqI (from left to right).
We prove the intermediate claim HxI: x ∈ order_interval X a d.
rewrite the current goal using HbEqI (from right to left).
An exact proof term for the current goal is Hxb.
We prove the intermediate claim HxX0: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λt0 : set ⇒ order_rel X a t0 ∧ order_rel X t0 d) x HxI).
We prove the intermediate claim HxConj: order_rel X a x ∧ order_rel X x d.
An exact proof term for the current goal is (SepE2 X (λt0 : set ⇒ order_rel X a t0 ∧ order_rel X t0 d) x HxI).
We prove the intermediate claim Hax: order_rel X a x.
An exact proof term for the current goal is (andEL (order_rel X a x) (order_rel X x d) HxConj).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (andER (order_rel X a x) (order_rel X x d) HxConj).
We prove the intermediate claim Had: order_rel X a d.
An exact proof term for the current goal is (order_rel_trans X a x d Hso HaX HxX0 HdX Hax Hxd).
An exact proof term for the current goal is (thm24_1_linear_continuum_intervals_connected X (order_topology X) a d Hlin0 HaX HdX Had).
Assume Hlow: ∃d ∈ X, b = {t ∈ X|order_rel X t d}.
Apply Hlow to the current goal.
Let d be given.
Assume HdCore.
We prove the intermediate claim HdX: d ∈ X.
An exact proof term for the current goal is (andEL (d ∈ X) (b = {t ∈ X|order_rel X t d}) HdCore).
We prove the intermediate claim HbEq: b = {t ∈ X|order_rel X t d}.
An exact proof term for the current goal is (andER (d ∈ X) (b = {t ∈ X|order_rel X t d}) HdCore).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim Hrays: connected_space {t ∈ X|order_rel X d t} (subspace_topology X (order_topology X) {t ∈ X|order_rel X d t}) ∧ connected_space {t ∈ X|order_rel X t d} (subspace_topology X (order_topology X) {t ∈ X|order_rel X t d}).
An exact proof term for the current goal is (thm24_1_linear_continuum_rays_connected X (order_topology X) d d Hlin0 HdX HdX).
An exact proof term for the current goal is (andER (connected_space {t ∈ X|order_rel X d t} (subspace_topology X (order_topology X) {t ∈ X|order_rel X d t})) (connected_space {t ∈ X|order_rel X t d} (subspace_topology X (order_topology X) {t ∈ X|order_rel X t d})) Hrays).
Assume Hup: ∃a ∈ X, b = {t ∈ X|order_rel X a t}.
Apply Hup to the current goal.
Let a be given.
Assume HaCore.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (andEL (a ∈ X) (b = {t ∈ X|order_rel X a t}) HaCore).
We prove the intermediate claim HbEq: b = {t ∈ X|order_rel X a t}.
An exact proof term for the current goal is (andER (a ∈ X) (b = {t ∈ X|order_rel X a t}) HaCore).
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim Hrays: connected_space {t ∈ X|order_rel X a t} (subspace_topology X (order_topology X) {t ∈ X|order_rel X a t}) ∧ connected_space {t ∈ X|order_rel X t a} (subspace_topology X (order_topology X) {t ∈ X|order_rel X t a}).
An exact proof term for the current goal is (thm24_1_linear_continuum_rays_connected X (order_topology X) a a Hlin0 HaX HaX).
An exact proof term for the current goal is (andEL (connected_space {t ∈ X|order_rel X a t} (subspace_topology X (order_topology X) {t ∈ X|order_rel X a t})) (connected_space {t ∈ X|order_rel X t a} (subspace_topology X (order_topology X) {t ∈ X|order_rel X t a})) Hrays).
Assume HbX: b = X.
rewrite the current goal using HbX (from left to right).
We prove the intermediate claim HTx0: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim Hsubeq: subspace_topology X (order_topology X) X = order_topology X.
An exact proof term for the current goal is (subspace_topology_whole X (order_topology X) HTx0).
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is (thm24_1_linear_continuum_connected X (order_topology X) Hlin0).
∎