for I being set
for m, n being bag of I holds n = (m -' (m -' n)) + (n -' m)