for X being set
for b1, b2 being bag of X holds
( b1 divides b2 iff ex b being bag of X st b2 = b1 + b )