theorem Th9: :: BAGORD_2:21

for I being set
for m, x, y being bag of I st x divides m & x <> y holds
m <> (m -' x) + y