Let X be given.

Assume Hso: simply_ordered_set X.

We will prove topology_on X (order_topology X).

An exact proof term for the current goal is (lemma_topology_from_basis X (order_topology_basis X) (order_topology_basis_is_basis X Hso)).

∎