theorem Th49: :: ORDERS_5:40

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