Definition. well_order_equi
well_order R M ↔ wf R M ∧ (∀x. ∀y. ∀z. (x, y) ∈ R → (y, z) ∈ R → (x, z) ∈ R) ∧ (∀x. ∀y. ¬(¬((x, y) ∈ R ↔ x = y) ↔ (y, x) ∈ R))