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

now

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

now

per cases ( max (b1 . k),(b2 . k) = b1 . k or max (b1 . k),(b2 . k) = b2 . k ) by XXREAL_0:16;

case max (b1 . k),(b2 . k) = b1 . k ; :: thesis: max (b1 . k),(b2 . k) <= b3 . k

hence max (b1 . k),(b2 . k) <= b3 . k by A1, POLYNOM1:def 13; :: thesis: verum

end;

case max (b1 . k),(b2 . k) = b2 . k ; :: thesis: max (b1 . k),(b2 . k) <= b3 . k

hence max (b1 . k),(b2 . k) <= b3 . k by A1, POLYNOM1:def 13; :: thesis: verum

end;

end;

end;

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

end;

hence lcm b1,b2 divides b3 by POLYNOM1:50; :: thesis: verum