theorem :: PRE_POLY:53

for X being set
for b being bag of X holds b + (EmptyBag X) = b