let Z be non empty set ; :: thesis: for B1, B2 being bag of Z holds
( B1 divides B2 iff ex B3 being bag of Z st B2 = B1 + B3 )
let b1, b2 be bag of Z; :: thesis: ( b1 divides b2 iff ex B3 being bag of Z st b2 = b1 + B3 )

now :: thesis: ( b1 divides b2 implies ex b3 being bag of Z st b2 = b1 + b3 )

assume A: b1 divides b2 ; :: thesis: ex b3 being bag of Z st b2 = b1 + b3
b1 + (b2 -' b1) = b2 by A, PRE_POLY:47;
hence ex b3 being bag of Z st b2 = b1 + b3 ; :: thesis: verum

end;

hence ( b1 divides b2 iff ex B3 being bag of Z st b2 = b1 + B3 ) by PRE_POLY:50; :: thesis: verum