theorem Th8: :: BAGORD_2:19

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