We will prove generated_topology_from_subbasis R (open_rays_subbasis R) = order_topology R.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis R (open_rays_subbasis R).
We will prove U ∈ order_topology R.
We prove the intermediate claim HS: subbasis_on R (open_rays_subbasis R).
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim HT: topology_on R (order_topology R).
An exact proof term for the current goal is order_topology_R_is_topology.
We prove the intermediate claim HSsub: open_rays_subbasis R ⊆ order_topology R.
An exact proof term for the current goal is open_rays_subbasis_sub_order_topology_R.
We prove the intermediate claim Hmin: finer_than (order_topology R) (generated_topology_from_subbasis R (open_rays_subbasis R)).
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal R (open_rays_subbasis R) (order_topology R) HS HT HSsub).
An exact proof term for the current goal is (Hmin U HU).
Let U be given.
Assume HU: U ∈ order_topology R.
We will prove U ∈ generated_topology_from_subbasis R (open_rays_subbasis R).
Set Tsub to be the term generated_topology_from_subbasis R (open_rays_subbasis R).
We prove the intermediate claim HS: subbasis_on R (open_rays_subbasis R).
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim HTsub: topology_on R Tsub.
An exact proof term for the current goal is (topology_from_subbasis_is_topology R (open_rays_subbasis R) HS).
We prove the intermediate claim HBsub: ∀b ∈ order_topology_basis R, 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 R b Hb).
We prove the intermediate claim Hfiner: finer_than Tsub (generated_topology R (order_topology_basis R)).
An exact proof term for the current goal is (generated_topology_finer_weak R (order_topology_basis R) Tsub HTsub HBsub).
An exact proof term for the current goal is (Hfiner U HU).
∎