Let X, a and b be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We will prove x ∈ (open_ray_upper X a) ∩ (open_ray_lower X b).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x Hx).
We prove the intermediate claim HxRel: order_rel X a x ∧ order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x Hx).
We prove the intermediate claim HxUp: x ∈ open_ray_upper X a.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0) x HxX (andEL (order_rel X a x) (order_rel X x b) HxRel)).
We prove the intermediate claim HxLo: x ∈ open_ray_lower X b.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b) x HxX (andER (order_rel X a x) (order_rel X x b) HxRel)).
An exact proof term for the current goal is (binintersectI (open_ray_upper X a) (open_ray_lower X b) x HxUp HxLo).
Let x be given.
Assume Hx: x ∈ (open_ray_upper X a) ∩ (open_ray_lower X b).
We will prove x ∈ {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We prove the intermediate claim HxUp: x ∈ open_ray_upper X a.
An exact proof term for the current goal is (binintersectE1 (open_ray_upper X a) (open_ray_lower X b) x Hx).
We prove the intermediate claim HxLo: x ∈ open_ray_lower X b.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper X a) (open_ray_lower X b) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0) x HxUp).
We prove the intermediate claim HxRelUp: order_rel X a x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a x0) x HxUp).
We prove the intermediate claim HxRelLo: order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 b) x HxLo).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxX (andI (order_rel X a x) (order_rel X x b) HxRelUp HxRelLo)).
∎