let X be set ; :: thesis: for b1, b2 being bag of X holds (b1 + b2) / b2 = b1
let b1, b2 be bag of X; :: thesis: (b1 + b2) / b2 = b1
b2 divides b1 + b2 by PRE_POLY:50;
then b2 + ((b1 + b2) / b2) = b1 + b2 by GROEB_2:def 1;
then (b2 + ((b1 + b2) / b2)) -' b2 = b1 by PRE_POLY:48;
hence (b1 + b2) / b2 = b1 by PRE_POLY:48; :: thesis: verum