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);

( 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 :: thesis: for k being object holds b1 . k <= (lcm (b1,b2)) . k

hence
b1 divides lcm (b1,b2)
by PRE_POLY:def 11; :: thesis: b2 divides lcm (b1,b2)let k be object ; :: 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;b1 . k <= max ((b1 . k),(b2 . k)) by XXREAL_0:25;

hence b1 . k <= (lcm (b1,b2)) . k by Def2; :: thesis: verum

now :: thesis: for k being object holds b2 . k <= (lcm (b1,b2)) . k

hence
b2 divides lcm (b1,b2)
by PRE_POLY:def 11; :: thesis: verumlet k be object ; :: 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;b2 . k <= max ((b1 . k),(b2 . k)) by XXREAL_0:25;

hence b2 . k <= (lcm (b1,b2)) . k by Def2; :: thesis: verum