Let X, a and b be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closed_interval_in X a b.
We will prove x ∈ (closed_ray_upper X a) ∩ (closed_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 ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hcond: (x = a ∨ order_rel X a x) ∧ (x = b ∨ order_rel X x b).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hleft: x = a ∨ order_rel X a x.
An exact proof term for the current goal is (andEL (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
We prove the intermediate claim Hright: x = b ∨ order_rel X x b.
An exact proof term for the current goal is (andER (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
Apply binintersectI to the current goal.
We will prove x ∈ closed_ray_upper X a.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ x0 = a ∨ order_rel X a x0) x HxX Hleft).
We will prove x ∈ closed_ray_lower X b.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ x0 = b ∨ order_rel X x0 b) x HxX Hright).
Let x be given.
Assume Hx: x ∈ (closed_ray_upper X a) ∩ (closed_ray_lower X b).
We will prove x ∈ closed_interval_in X a b.
We prove the intermediate claim Hpair: x ∈ closed_ray_upper X a ∧ x ∈ closed_ray_lower X b.
An exact proof term for the current goal is (binintersectE (closed_ray_upper X a) (closed_ray_lower X b) x Hx).
We prove the intermediate claim HxUp: x ∈ closed_ray_upper X a.
An exact proof term for the current goal is (andEL (x ∈ closed_ray_upper X a) (x ∈ closed_ray_lower X b) Hpair).
We prove the intermediate claim HxLow: x ∈ closed_ray_lower X b.
An exact proof term for the current goal is (andER (x ∈ closed_ray_upper X a) (x ∈ closed_ray_lower X b) Hpair).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 = a ∨ order_rel X a x0) x HxUp).
We prove the intermediate claim Hleft: x = a ∨ order_rel X a x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 = a ∨ order_rel X a x0) x HxUp).
We prove the intermediate claim Hright: x = b ∨ order_rel X x b.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 = b ∨ order_rel X x0 b) x HxLow).
We prove the intermediate claim Hdef: closed_interval_in X a b = {x0 ∈ X|(x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x HxX (andI (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hleft Hright)).
∎