Let X, Tx, C and x be given.

Assume Hlin: linear_continuum X Tx.

Assume HCcl: closed_in X Tx C.

Assume HCne: C ≠ Empty.

Assume HxXC: x ∈ (X ∖ C).

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 D to be the term X ∖ C.

Set Td to be the term subspace_topology X Tx D.

Set U to be the term component_of D Td x.

We prove the intermediate claim HUdef: U = component_of D Td x.

Use reflexivity.

We prove the intermediate claim HxD: x ∈ D.

An exact proof term for the current goal is HxXC.

The rest of this subproof is missing.

∎