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