Let X, a and b be given.

Let x be given.

Assume Hx: x ∈ order_interval X a b.

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

∎