theorem Th51: :: ORDERS_5:42

for A being set
for D being a_partition of A holds D = the carrier of (QuotientOrder (PreorderFromPartition D))