Let X, a, b and x be given.

Assume Hx: x ∈ order_interval X a b.

Apply andI to the current goal.

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).

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).

∎