po_trans

Theorem po_trans

Theorem. po_trans
partial_order R M → x ∈ M → y ∈ M → z ∈ M → R x y → R y z → R x z

Proof
01. 1 ⊢ partial_order R M, hypo.
02. 1 ⊢ ∀x. ∀y. ∀z. x ∈ M → y ∈ M → z ∈ M →
  R x y → R y z → R x z, lsubj_conj_elimr po_equi 1.
03. 1 ⊢ ∀y. ∀z. x ∈ M → y ∈ M → z ∈ M →
  R x y → R y z → R x z, uq_elim 2.
04. 1 ⊢ ∀z. x ∈ M → y ∈ M → z ∈ M →
  R x y → R y z → R x z, uq_elim 3.
05. 1 ⊢ x ∈ M → y ∈ M → z ∈ M →
  R x y → R y z → R x z, uq_elim 4.
po_trans. ⊢ partial_order R M → x ∈ M → y ∈ M → z ∈ M →
  R x y → R y z → R x z, subj_intro 5.