let X be set ; :: thesis: for b1, b2, b3 being bag of X st lcm b2,b1 divides lcm b2,b3 holds
lcm b1,b3 divides lcm b2,b3
let b1, b2, b3 be bag of X; :: thesis: ( lcm b2,b1 divides lcm b2,b3 implies lcm b1,b3 divides lcm b2,b3 )
assume A1: lcm b2,b1 divides lcm b2,b3 ; :: thesis: lcm b1,b3 divides lcm b2,b3
for k being set st k in X holds
(lcm b1,b3) . k <= (lcm b2,b3) . k

proof

let k be set ; :: thesis: ( k in X implies (lcm b1,b3) . k <= (lcm b2,b3) . k )
assume k in X ; :: thesis: (lcm b1,b3) . k <= (lcm b2,b3) . k
A2: b3 . k <= max (b2 . k),(b3 . k) by XXREAL_0:25;
(lcm b2,b1) . k <= (lcm b2,b3) . k by A1, PRE_POLY:def 11;
then max (b2 . k),(b1 . k) <= (lcm b2,b3) . k by Def2;
then A3: max (b2 . k),(b1 . k) <= max (b2 . k),(b3 . k) by Def2;
b1 . k <= max (b2 . k),(b1 . k) by XXREAL_0:25;
then b1 . k <= max (b2 . k),(b3 . k) by A3, XXREAL_0:2;
then max (b1 . k),(b3 . k) <= max (b2 . k),(b3 . k) by A2, XXREAL_0:28;
then max (b1 . k),(b3 . k) <= (lcm b2,b3) . k by Def2;
hence (lcm b1,b3) . k <= (lcm b2,b3) . k by Def2; :: thesis: verum

end;

hence lcm b1,b3 divides lcm b2,b3 by PRE_POLY:46; :: thesis: verum