theorem Th37: :: ORDERS_5:28

for A being LinearOrder holds the InternalRel of A linearly_orders the carrier of A