:: deftheorem Def1 defines / GROEB_2:def 1 :
for X being set
for b1, b2 being bag of X st b2 divides b1 holds
for b₄ being bag of X holds
( b₄ = b1 / b2 iff b2 + b₄ = b1 );