theorem Th15: :: BAGORD_2:27

for I being set
for k, x1, x2, y1, y2 being bag of I st x2 divides k & x1 divides (k -' x2) + y2 holds
( x2 + (x1 -' y2) divides k & (((k -' x2) + y2) -' x1) + y1 = (k -' (x2 + (x1 -' y2))) + ((y2 -' x1) + y1) )