Definition. is_supremum_equi
is_supremum R M y A ↔ (∀x. x ∈ A → R x y) ∧ (∀b. b ∈ M → (∀x. x ∈ A → R x b) → R y b)