theorem :: PRE_POLY:60

for n being Ordinal
for b being bag of n holds EmptyBag n <=' b by Th48, Th57;