theorem Th42: :: ORDERS_5:33

for A being Order holds EqRelOf A = id the carrier of A