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