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