Let X and b be given.
Assume HbX.
We will prove open_ray_lower X b ∈ order_topology_basis X.
Set U to be the term open_ray_lower X b.
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 x0 b) x HxU).
We prove the intermediate claim HUex: ∃b0 ∈ X, U = {x ∈ X|order_rel X x b0}.
We use b to witness the existential quantifier.
We will prove b ∈ X ∧ U = {x ∈ X|order_rel X x b}.
Apply andI to the current goal.
An exact proof term for the current goal is HbX.
Use reflexivity.
We prove the intermediate claim HUfam: U ∈ {I ∈ đ’Ģ X|∃b0 ∈ X, I = {x ∈ X|order_rel X x b0}}.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}) U HUpow HUex).
We prove the intermediate claim HUold: U ∈ Bold.
An exact proof term for the current goal is (binunionI1 ({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 (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}} U HUfam)).
An exact proof term for the current goal is (binunionI1 Bold {X} U HUold).
∎