theorem Th29: :: ORDERS_1:29

for R being Relation
for X being set st R linearly_orders X holds
( R quasi_orders X & R partially_orders X ) ;