theorem Th27A: :: BAGORD_2:46

for I, J being set
for m being bag of I holds support (m -' (m | J)) = (support m) \ J