for n being set
for b1, b2 being bag of n st b1 divides b2 & b2 -' b1 = EmptyBag n holds
b2 = b1