Let X be given.
Set Tsub to be the term generated_topology_from_subbasis X (open_rays_subbasis X).
We prove the intermediate claim HSsub: 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) HSsub).
We will prove order_topology_basis X ⊆ Tsub.
Let I be given.
Assume HI: I ∈ order_topology_basis X.
We will prove I ∈ Tsub.
Set Bold to be the term (({I0 ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} âˆĒ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}}) âˆĒ {I0 ∈ đ’Ģ X|∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}}).
Apply (binunionE' Bold {X} I (I ∈ Tsub)) to the current goal.
Assume HIold: I ∈ Bold.
Apply (binunionE' ({I0 ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} âˆĒ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}}) {I0 ∈ đ’Ģ X|∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}} I (I ∈ Tsub)) to the current goal.
Assume HI0: I ∈ ({I0 ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} âˆĒ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}}).
Apply (binunionE' {I0 ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}} I (I ∈ Tsub)) to the current goal.
Assume HIint: I ∈ {I0 ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}}.
We prove the intermediate claim Hex: ∃a0 ∈ X, ∃b0 ∈ X, I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}) I HIint).
Apply Hex to the current goal.
Let a0 be given.
Assume Hcore: a0 ∈ X ∧ ∃b0 ∈ X, I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}.
Apply Hcore to the current goal.
Assume HaX: a0 ∈ X.
Assume Hexb: ∃b0 ∈ X, I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}.
Apply Hexb to the current goal.
Let b0 be given.
Assume Hcore2: b0 ∈ X ∧ I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}.
Apply Hcore2 to the current goal.
Assume HbX: b0 ∈ X.
Assume HIeq: I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}.
rewrite the current goal using HIeq (from left to right).
Set U1 to be the term open_ray_upper X a0.
Set U2 to be the term open_ray_lower X b0.
We prove the intermediate claim HU1S: U1 ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X a0 HaX).
We prove the intermediate claim HU2S: U2 ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X b0 HbX).
We prove the intermediate claim HU1open: U1 ∈ Tsub.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U1 HSsub HU1S).
We prove the intermediate claim HU2open: U2 ∈ Tsub.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U2 HSsub HU2S).
We prove the intermediate claim Heq: {x ∈ X|order_rel X a0 x ∧ order_rel X x b0} = U1 ∊ U2.
An exact proof term for the current goal is (open_interval_eq_rays_intersection X a0 b0).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tsub U1 U2 HTsub HU1open HU2open).
Assume HIlow: I ∈ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}}.
We prove the intermediate claim Hex: ∃b0 ∈ X, I = {x ∈ X|order_rel X x b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}) I HIlow).
Apply Hex to the current goal.
Let b0 be given.
Assume Hcore: b0 ∈ X ∧ I = {x ∈ X|order_rel X x b0}.
Apply Hcore to the current goal.
Assume HbX: b0 ∈ X.
Assume HIeq: I = {x ∈ X|order_rel X x b0}.
rewrite the current goal using HIeq (from left to right).
We prove the intermediate claim Hdef: open_ray_lower X b0 = {x ∈ X|order_rel X x b0}.
Use reflexivity.
rewrite the current goal using Hdef (from right to left).
Set U to be the term open_ray_lower X b0.
We prove the intermediate claim HUS: U ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X b0 HbX).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U HSsub HUS).
An exact proof term for the current goal is HI0.
Assume HIup: I ∈ {I0 ∈ đ’Ģ X|∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}}.
We prove the intermediate claim Hex: ∃a0 ∈ X, I = {x ∈ X|order_rel X a0 x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}) I HIup).
Apply Hex to the current goal.
Let a0 be given.
Assume Hcore: a0 ∈ X ∧ I = {x ∈ X|order_rel X a0 x}.
Apply Hcore to the current goal.
Assume HaX: a0 ∈ X.
Assume HIeq: I = {x ∈ X|order_rel X a0 x}.
rewrite the current goal using HIeq (from left to right).
We prove the intermediate claim Hdef: open_ray_upper X a0 = {x ∈ X|order_rel X a0 x}.
Use reflexivity.
rewrite the current goal using Hdef (from right to left).
Set U to be the term open_ray_upper X a0.
We prove the intermediate claim HUS: U ∈ open_rays_subbasis X.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X a0 HaX).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis X (open_rays_subbasis X) U HSsub HUS).
An exact proof term for the current goal is HIold.
Assume HIX: I ∈ {X}.
We prove the intermediate claim HIeq: I = X.
An exact proof term for the current goal is (SingE X I HIX).
rewrite the current goal using HIeq (from left to right).
An exact proof term for the current goal is (topology_has_X X Tsub HTsub).
An exact proof term for the current goal is HI.
∎