Proof 01. 1 ⊢ partial_order R M, hypo. 02. 1 ⊢ ∀x. x ∈ M → R x x, lsubj_conj_elimll po_equi 1. 03. 1 ⊢ x ∈ M → R x x, uq_elim 2. po_refl. ⊢ partial_order R M → x ∈ M → R x x, subj_intro 3.