theorem Th50: :: ORDERS_5:41

for A being set
for D being a_partition of A holds D = Class (EqRelOf (PreorderFromPartition D))