theorem Th54: :: PRE_POLY:56

for X being set
for b being bag of X holds b -' b = EmptyBag X