Definition. is_min_equi
is_min R y A ↔ y ∈ A ∧ ∀x. x ∈ A → R y x