Let X, Tx, A, B, C, x, a and b be given.
Assume Hlin: linear_continuum X Tx.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume HAB: A ∩ B = Empty.
Assume HCcl: closed_in X Tx C.
Assume HaA: a ∈ A.
Assume HbB: b ∈ B.
Assume HxXC: x ∈ (X ∖ C).
Assume HaComp: a ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.
Assume HbComp: b ∈ component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is (linear_continuum_simply_ordered X Tx Hlin).
We prove the intermediate claim HTxeq: Tx = order_topology X.
An exact proof term for the current goal is (linear_continuum_order_topology_eq X Tx Hlin).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (linear_continuum_topology_on X Tx Hlin).
Set V to be the term component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.
We prove the intermediate claim HVdef: V = component_of (X ∖ C) (subspace_topology X Tx (X ∖ C)) x.
Use reflexivity.
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HaComp.
We prove the intermediate claim HbV: b ∈ V.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HbComp.
The rest of this subproof is missing.
∎