let X be set ; :: thesis: for b1, b2, b3 being bag of X st lcm (b1,b3) divides lcm (b2,b3) holds
b1 divides lcm (b2,b3)
let b1, b2, b3 be bag of X; :: thesis: ( lcm (b1,b3) divides lcm (b2,b3) implies b1 divides lcm (b2,b3) )
assume A1: lcm (b1,b3) divides lcm (b2,b3) ; :: thesis: b1 divides lcm (b2,b3)
for k being object st k in X holds
b1 . k <= (lcm (b2,b3)) . k
proof
let k be object ; :: thesis: ( k in X implies b1 . k <= (lcm (b2,b3)) . k )
assume k in X ; :: thesis: b1 . k <= (lcm (b2,b3)) . k
(lcm (b1,b3)) . k <= (lcm (b2,b3)) . k by A1, PRE_POLY:def 11;
then max ((b1 . k),(b3 . k)) <= (lcm (b2,b3)) . k by Def2;
then A2: max ((b1 . k),(b3 . k)) <= max ((b2 . k),(b3 . k)) by Def2;
b1 . k <= max ((b1 . k),(b3 . k)) by XXREAL_0:25;
then b1 . k <= max ((b2 . k),(b3 . k)) by A2, XXREAL_0:2;
hence b1 . k <= (lcm (b2,b3)) . k by Def2; :: thesis: verum
end;
hence b1 divides lcm (b2,b3) by PRE_POLY:46; :: thesis: verum