Let X and Tx be given.

Assume Hlin: linear_continuum X Tx.

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 Heq: Tx = order_topology X.

An exact proof term for the current goal is (linear_continuum_order_topology_eq X Tx Hlin).

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is (order_topology_is_topology X Hso).

∎