Definition. is_max_equi
is_max R y A ↔ y ∈ A ∧ ∀x. x ∈ A → R x y