Let U be given.
Assume HU: U ∈ open_rays_subbasis R.
We will prove U ∈ order_topology R.
Apply (binunionE' ({I0 ∈ đ’Ģ R|∃a ∈ R, I0 = open_ray_upper R a} âˆĒ {I0 ∈ đ’Ģ R|∃b ∈ R, I0 = open_ray_lower R b}) {R} U (U ∈ order_topology R)) to the current goal.
Assume HU0: U ∈ ({I0 ∈ đ’Ģ R|∃a ∈ R, I0 = open_ray_upper R a} âˆĒ {I0 ∈ đ’Ģ R|∃b ∈ R, I0 = open_ray_lower R b}).
Apply (binunionE' {I0 ∈ đ’Ģ R|∃a ∈ R, I0 = open_ray_upper R a} {I0 ∈ đ’Ģ R|∃b ∈ R, I0 = open_ray_lower R b} U (U ∈ order_topology R)) to the current goal.
Assume HUup: U ∈ {I0 ∈ đ’Ģ R|∃a ∈ R, I0 = open_ray_upper R a}.
We prove the intermediate claim Hex: ∃a ∈ R, U = open_ray_upper R a.
An exact proof term for the current goal is (SepE2 (đ’Ģ R) (ÎģI0 : set ⇒ ∃a ∈ R, I0 = open_ray_upper R a) U HUup).
Apply Hex to the current goal.
Let a be given.
Assume Hacore.
Apply Hacore to the current goal.
Assume HaR: a ∈ R.
Assume HUeq: U = open_ray_upper R a.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HUbasis: open_ray_upper R a ∈ order_topology_basis R.
An exact proof term for the current goal is (open_ray_upper_in_order_topology_basis R a HaR).
We prove the intermediate claim HUpow: open_ray_upper R a ∈ đ’Ģ R.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE1 R (Îģx0 : set ⇒ order_rel R a x0) x HxU).
An exact proof term for the current goal is (generated_topology_contains_elem R (order_topology_basis R) (open_ray_upper R a) HUpow HUbasis).
Assume HUlow: U ∈ {I0 ∈ đ’Ģ R|∃b ∈ R, I0 = open_ray_lower R b}.
We prove the intermediate claim Hex: ∃b ∈ R, U = open_ray_lower R b.
An exact proof term for the current goal is (SepE2 (đ’Ģ R) (ÎģI0 : set ⇒ ∃b ∈ R, I0 = open_ray_lower R b) U HUlow).
Apply Hex to the current goal.
Let b be given.
Assume Hbcore.
Apply Hbcore to the current goal.
Assume HbR: b ∈ R.
Assume HUeq: U = open_ray_lower R b.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HUbasis: open_ray_lower R b ∈ order_topology_basis R.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis R b HbR).
We prove the intermediate claim HUpow: open_ray_lower R b ∈ đ’Ģ R.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE1 R (Îģx0 : set ⇒ order_rel R x0 b) x HxU).
An exact proof term for the current goal is (generated_topology_contains_elem R (order_topology_basis R) (open_ray_lower R b) HUpow HUbasis).
An exact proof term for the current goal is HU0.
Assume HUR: U ∈ {R}.
We prove the intermediate claim HUeq: U = R.
An exact proof term for the current goal is (SingE R U HUR).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_has_X R (order_topology R) order_topology_R_is_topology).
An exact proof term for the current goal is HU.
∎