po_antisym

Theorem po_antisym

Theorem. po_antisym
partial_order R M → x ∈ M → y ∈ M → R x y → R y x → x = y

Proof
01. 1 ⊢ partial_order R M, hypo.
02. 1 ⊢ ∀x. ∀y. x ∈ M → y ∈ M → R x y → R y x → x = y,
  lsubj_conj_elimlr po_equi 1.
03. 1 ⊢ ∀y. x ∈ M → y ∈ M → R x y → R y x → x = y, uq_elim 2.
04. 1 ⊢ x ∈ M → y ∈ M → R x y → R y x → x = y, uq_elim 3.
po_antisym. ⊢ partial_order R M → x ∈ M → y ∈ M →
  R x y → R y x → x = y, subj_intro 4.