:: deftheorem defines zero TERMORD:def 1 :
for X being set
for b being bag of X holds
( b is zero iff b = EmptyBag X );