theorem Th28: :: ORDERS_1:28

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