theorem :: BAGORD_2:45

for I, J being set
for m being bag of I st support m c= J holds
m | J = m