An exact proof term for the current goal is (andER (Y ⊆ X) (∀a b : set, a ∈ Y → b ∈ Y → order_interval X a b ⊆ Y) H).