Let X and b be given.
Assume HbX.
Set U to be the term open_ray_lower X b.
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 = open_ray_lower X b0.
We use b to witness the existential quantifier.
We will prove b ∈ X ∧ U = open_ray_lower 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 ∈ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = open_ray_lower X b0}.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = open_ray_lower X b0) U HUpow HUex).
An exact proof term for the current goal is (binunionI1 ({I0 ∈ đ’Ģ X|∃a0 ∈ X, I0 = open_ray_upper X a0} âˆĒ {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = open_ray_lower X b0}) {X} U (binunionI2 {I0 ∈ đ’Ģ X|∃a0 ∈ X, I0 = open_ray_upper X a0} {I0 ∈ đ’Ģ X|∃b0 ∈ X, I0 = open_ray_lower X b0} U HUfam)).
∎