Definition. is_infimum_equi
is_infimum R M y A ↔ (∀x. x ∈ A → R y x) ∧ (∀b. b ∈ M → (∀x. x ∈ A → R b x) → R b y)