We will prove topology_on ω (order_topology ω).

An exact proof term for the current goal is (lemma_topology_from_basis ω (order_topology_basis ω) order_topology_basis_omega_is_basis).

∎