let X be set ; :: thesis: for b1, b2 being bag of X holds
( b1 divides lcm b1,b2 & b2 divides lcm b1,b2 )
let b1, b2 be bag of X; :: thesis: ( b1 divides lcm b1,b2 & b2 divides lcm b1,b2 )
set bb = lcm b1,b2;

now

let k be set ; :: thesis: b1 . k <= (lcm b1,b2) . k
b1 . k <= max (b1 . k),(b2 . k) by XXREAL_0:25;
hence b1 . k <= (lcm b1,b2) . k by Def2; :: thesis: verum

end;

hence b1 divides lcm b1,b2 by PRE_POLY:def 11; :: thesis: b2 divides lcm b1,b2

now

let k be set ; :: thesis: b2 . k <= (lcm b1,b2) . k
b2 . k <= max (b1 . k),(b2 . k) by XXREAL_0:25;
hence b2 . k <= (lcm b1,b2) . k by Def2; :: thesis: verum

end;

hence b2 divides lcm b1,b2 by PRE_POLY:def 11; :: thesis: verum