let X be set ; :: thesis:
let b1, b2 be bag of X; :: thesis:
set bb = lcm (b1,b2);

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

end;

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

end;