:: deftheorem defines PreorderFromPartition ORDERS_5:def 10 :
for A being set
for D being a_partition of A holds PreorderFromPartition D = RelStr(# A,(ERl D) #);