Definition. po_equi
partial_order R M ↔ (∀x. x ∈ M → R x x) ∧ (∀x. ∀y. x ∈ M → y ∈ M → R x y → R y x → x = y) ∧ (∀x. ∀y. ∀z. x ∈ M → y ∈ M → z ∈ M → R x y → R y z → R x z)