theorem :: POLYNOM7:3

for b being bag of {} holds b = EmptyBag {}