theorem Th8A: :: BAGORD_2:20

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