theorem Th47: :: ORDERS_5:38

for A being Preorder holds the carrier of (QuotientOrder A) is a_partition of the carrier of A