theorem Lem3: :: BAGORD_2:25

for I being set
for m, n being bag of I holds m -' n divides m