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