let a, b be Integer; :: thesis: a lcm b = (abs a) lcm (abs b)
A1: ( abs a = a or abs a = - a ) by ABSVALUE:1;
a divides a lcm b by Def2;
then A2: abs a divides a lcm b by A1, Th14;
A3: ( abs b = b or abs b = - b ) by ABSVALUE:1;
b divides a lcm b by Def2;
then A4: abs b divides a lcm b by A3, Th14;

now

let m be Integer; :: thesis: ( abs a divides m & abs b divides m implies a lcm b divides m )
assume ( abs a divides m & abs b divides m ) ; :: thesis: a lcm b divides m
then ( a divides m & b divides m ) by A1, A3, Th14;
hence a lcm b divides m by Def2; :: thesis: verum

end;

hence a lcm b = (abs a) lcm (abs b) by A2, A4, Def2; :: thesis: verum