theorem :: BAGORD_2:62

for R being non empty transitive asymmetric RelStr
for a, b, c, d being Element of (DershowitzMannaOrder R)
for e being bag of the carrier of R st a <= b & e divides a & e divides b & c = a -' e & d = b -' e holds
c <= d