let X be set ; :: thesis: for b1, b2, b3 being bag of X st b1 divides lcm (b2,b3) holds

lcm (b2,b1) divides lcm (b2,b3)

let b1, b2, b3 be bag of X; :: thesis: ( b1 divides lcm (b2,b3) implies lcm (b2,b1) divides lcm (b2,b3) )

assume A1: b1 divides lcm (b2,b3) ; :: thesis: lcm (b2,b1) divides lcm (b2,b3)

for k being object st k in X holds

(lcm (b2,b1)) . k <= (lcm (b2,b3)) . k

lcm (b2,b1) divides lcm (b2,b3)

let b1, b2, b3 be bag of X; :: thesis: ( b1 divides lcm (b2,b3) implies lcm (b2,b1) divides lcm (b2,b3) )

assume A1: b1 divides lcm (b2,b3) ; :: thesis: lcm (b2,b1) divides lcm (b2,b3)

for k being object st k in X holds

(lcm (b2,b1)) . k <= (lcm (b2,b3)) . k

proof

hence
lcm (b2,b1) divides lcm (b2,b3)
by PRE_POLY:46; :: thesis: verum
let k be object ; :: thesis: ( k in X implies (lcm (b2,b1)) . k <= (lcm (b2,b3)) . k )

assume k in X ; :: thesis: (lcm (b2,b1)) . k <= (lcm (b2,b3)) . k

b1 . k <= (lcm (b2,b3)) . k by A1, PRE_POLY:def 11;

then A2: b1 . k <= max ((b2 . k),(b3 . k)) by Def2;

b2 . k <= max ((b2 . k),(b3 . k)) by XXREAL_0:25;

then max ((b2 . k),(b1 . k)) <= max ((b2 . k),(b3 . k)) by A2, XXREAL_0:28;

then max ((b2 . k),(b1 . k)) <= (lcm (b2,b3)) . k by Def2;

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

end;assume k in X ; :: thesis: (lcm (b2,b1)) . k <= (lcm (b2,b3)) . k

b1 . k <= (lcm (b2,b3)) . k by A1, PRE_POLY:def 11;

then A2: b1 . k <= max ((b2 . k),(b3 . k)) by Def2;

b2 . k <= max ((b2 . k),(b3 . k)) by XXREAL_0:25;

then max ((b2 . k),(b1 . k)) <= max ((b2 . k),(b3 . k)) by A2, XXREAL_0:28;

then max ((b2 . k),(b1 . k)) <= (lcm (b2,b3)) . k by Def2;

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