theorem Th47: :: ORDERS_5:38
for A being Preorder holds the carrier of (QuotientOrder A) is a_partition of the carrier of A