theorem :: BAGORD_2:43

for I, J being set
for m being bag of I holds (m | J) + (m | (I \ J)) = m