theorem :: ORDERS_1:30

for R being Relation
for X being set st R partially_orders X holds
R quasi_orders X ;