Let X be given.
Assume Hso: simply_ordered_set X.
We will prove open_rays_subbasis X ⊆ order_topology X.
Let U be given.
Assume HU: U ∈ open_rays_subbasis X.
We will prove U ∈ order_topology X.
Apply (binunionE' ({I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}) {X} U (U ∈ order_topology X)) to the current goal.
Assume HU0: U ∈ ({I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}).
Apply (binunionE' {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a} {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b} U (U ∈ order_topology X)) to the current goal.
Assume HU1: U ∈ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = open_ray_upper X a}.
We prove the intermediate claim Hex: ∃a ∈ X, U = open_ray_upper X a.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, I0 = open_ray_upper X a) U HU1).
Apply Hex to the current goal.
Let a be given.
Assume Hcore: a ∈ X ∧ U = open_ray_upper X a.
Apply Hcore to the current goal.
Assume HaX: a ∈ X.
Assume HUeq: U = open_ray_upper X a.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HUinB: open_ray_upper X a ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_upper_in_order_topology_basis X a HaX).
We prove the intermediate claim HUpow: open_ray_upper X a ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ open_ray_upper X a.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a x0) x HxU).
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) (open_ray_upper X a) HUpow HUinB).
Assume HU2: U ∈ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = open_ray_lower X b}.
We prove the intermediate claim Hex: ∃b ∈ X, U = open_ray_lower X b.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b ∈ X, I0 = open_ray_lower X b) U HU2).
Apply Hex to the current goal.
Let b be given.
Assume Hcore: b ∈ X ∧ U = open_ray_lower X b.
Apply Hcore to the current goal.
Assume HbX: b ∈ X.
Assume HUeq: U = open_ray_lower X b.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HUinB: open_ray_lower X b ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X b HbX).
We prove the intermediate claim HUpow: open_ray_lower X b ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ open_ray_lower X b.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 b) x HxU).
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) (open_ray_lower X b) HUpow HUinB).
An exact proof term for the current goal is HU0.
Assume HUX: U ∈ {X}.
We prove the intermediate claim HUeq: U = X.
An exact proof term for the current goal is (SingE X U HUX).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_has_X X (order_topology X) (order_topology_is_topology X Hso)).
An exact proof term for the current goal is HU.
∎