Let X and a be given.
Assume HaX.
We will prove open_ray_upper X a ∈ order_topology_basis X.
Set U to be the term open_ray_upper X a.
Set Bold to be the term ({I ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} âˆĒ {I ∈ đ’Ģ X|∃b0 ∈ X, I = {x ∈ X|order_rel X x b0}} âˆĒ {I ∈ đ’Ģ X|∃a0 ∈ X, I = {x ∈ X|order_rel X a0 x}}).
We prove the intermediate claim HUpow: U ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let x be given.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a x0) x HxU).
We prove the intermediate claim HUex: ∃a0 ∈ X, U = {x ∈ X|order_rel X a0 x}.
We use a to witness the existential quantifier.
We will prove a ∈ X ∧ U = {x ∈ X|order_rel X a x}.
Apply andI to the current goal.
An exact proof term for the current goal is HaX.
Use reflexivity.
We prove the intermediate claim HUfam: U ∈ {I ∈ đ’Ģ X|∃a0 ∈ X, I = {x ∈ X|order_rel X a0 x}}.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}) U HUpow HUex).
We prove the intermediate claim HUold: U ∈ Bold.
An exact proof term for the current goal is (binunionI2 ({I ∈ đ’Ģ X|∃a0 ∈ X, ∃b0 ∈ X, I = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}} âˆĒ {I ∈ đ’Ģ X|∃b0 ∈ X, I = {x ∈ X|order_rel X x b0}}) {I ∈ đ’Ģ X|∃a0 ∈ X, I = {x ∈ X|order_rel X a0 x}} U HUfam).
An exact proof term for the current goal is (binunionI1 Bold {X} U HUold).
∎