let X be set ; 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; ( b1 divides lcm (b1,b2) & b2 divides lcm (b1,b2) )
set bb = lcm (b1,b2);
hence
b1 divides lcm (b1,b2)
by PRE_POLY:def 11; b2 divides lcm (b1,b2)
hence
b2 divides lcm (b1,b2)
by PRE_POLY:def 11; verum