theorem :: ORDERS_1:17

for R being Relation st R is being_partial-order holds
R ~ is being_partial-order ;