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