theorem Th18: :: ORDERS_1:18

for R being Relation st R is being_linear-order holds
R ~ is being_linear-order by Lm5;