for n being Ordinal
for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )