theorem Th1: :: GROEB_3:1

for X being set
for b1, b2 being bag of X holds (b1 + b2) / b2 = b1