Proof wf_unfold. ⊢ wf R M → ∀A. A ⊆ M → ¬A = ∅ → ∃y. y ∈ A ∧ ¬∃x. x ∈ A ∧ (x, y) ∈ R, bij_eliml wf_equi.