let X be set ; :: thesis: for b1, b2, b3 being bag of X st b1 divides b3 & b2 divides b3 holds
lcm (b1,b2) divides b3
let b1, b2, b3 be bag of X; :: thesis: ( b1 divides b3 & b2 divides b3 implies lcm (b1,b2) divides b3 )
assume that
A1: b1 divides b3 and
A2: b2 divides b3 ; :: thesis: lcm (b1,b2) divides b3
now :: thesis: for k being object st k in X holds
(lcm (b1,b2)) . k <= b3 . k
let k be object ; :: thesis: ( k in X implies (lcm (b1,b2)) . k <= b3 . k )
assume k in X ; :: thesis: (lcm (b1,b2)) . k <= b3 . k
now :: thesis: ( ( max ((b1 . k),(b2 . k)) = b1 . k & max ((b1 . k),(b2 . k)) <= b3 . k ) or ( max ((b1 . k),(b2 . k)) = b2 . k & max ((b1 . k),(b2 . k)) <= b3 . k ) )
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, PRE_POLY:def 11; :: 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 A2, PRE_POLY:def 11; :: thesis: verum
end;
end;
end;
hence (lcm (b1,b2)) . k <= b3 . k by Def2; :: thesis: verum
end;
hence lcm (b1,b2) divides b3 by PRE_POLY:46; :: thesis: verum