:: deftheorem defines being_partial-order ORDERS_1:def 5 :
for R being Relation holds
( R is being_partial-order iff ( R is reflexive & R is transitive & R is antisymmetric ) );