:: deftheorem defines partially_orders ORDERS_1:def 8 :
for R being Relation
for X being set holds
( R partially_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X ) );