Let X and Tx be given.
Assume Hlin: linear_continuum X Tx.
Set P to be the term simply_ordered_set X.
Set Q to be the term Tx = order_topology X.
Set R to be the term ∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y.
Set S to be the term ∀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.
Set T to be the term ∀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).
We prove the intermediate claim H1: (((P ∧ Q) ∧ R) ∧ S).
An exact proof term for the current goal is (andEL (((P ∧ Q) ∧ R) ∧ S) T Hlin).
We prove the intermediate claim H2: ((P ∧ Q) ∧ R).
An exact proof term for the current goal is (andEL ((P ∧ Q) ∧ R) S H1).
We prove the intermediate claim HPQ: (P ∧ Q).
An exact proof term for the current goal is (andEL (P ∧ Q) R H2).
An exact proof term for the current goal is (andER P Q HPQ).
∎