let R be Relation; :: thesis: ( R is being_partial-order implies R is being_quasi-order )
assume that
A1: R is reflexive and
A2: R is transitive and
R is antisymmetric ; :: according to ORDERS_1:def 4 :: thesis: R is being_quasi-order
thus ( R is reflexive & R is transitive ) by A1, A2; :: according to ORDERS_1:def 3 :: thesis: verum