for n being set
for b being bag of n holds EmptyBag n divides b ;