Let X be given.
Assume Hso: simply_ordered_set X.
We will prove generated_topology_from_subbasis X (open_rays_subbasis X) = order_topology X.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis X (open_rays_subbasis X).
We will prove U ∈ order_topology X.
We prove the intermediate claim HS: subbasis_on X (open_rays_subbasis X).
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X).
We prove the intermediate claim HT: topology_on X (order_topology X).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HSsub: open_rays_subbasis X ⊆ order_topology X.
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology X Hso).
We prove the intermediate claim Hmin: finer_than (order_topology X) (generated_topology_from_subbasis X (open_rays_subbasis X)).
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal X (open_rays_subbasis X) (order_topology X) HS HT HSsub).
An exact proof term for the current goal is (Hmin U HU).
Let U be given.
Assume HU: U ∈ order_topology X.
We will prove U ∈ generated_topology_from_subbasis X (open_rays_subbasis X).
Set Tsub to be the term generated_topology_from_subbasis X (open_rays_subbasis X).
We prove the intermediate claim HS: subbasis_on X (open_rays_subbasis X).
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X).
We prove the intermediate claim HTsub: topology_on X Tsub.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X (open_rays_subbasis X) HS).
We prove the intermediate claim HBsub: ∀b ∈ order_topology_basis X, b ∈ Tsub.
Let b be given.
Assume Hb.
An exact proof term for the current goal is (order_topology_basis_sub_generated_from_open_rays X b Hb).
We prove the intermediate claim Hfiner: finer_than Tsub (generated_topology X (order_topology_basis X)).
An exact proof term for the current goal is (generated_topology_finer_weak X (order_topology_basis X) Tsub HTsub HBsub).
An exact proof term for the current goal is (Hfiner U HU).
∎