let a, b be Integer; :: thesis: a lcm b = (abs a) lcm (abs b)
A1: ( abs b = b or abs b = - b ) by ABSVALUE:1;
A2: ( abs a = a or abs a = - a ) by ABSVALUE:1;

A3: 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 A2, A1, Th14;
hence a lcm b divides m by Def2; :: thesis: verum

end;

b divides a lcm b by Def2;
then A4: abs b divides a lcm b by A1, Th14;
a divides a lcm b by Def2;
then abs a divides a lcm b by A2, Th14;
hence a lcm b = (abs a) lcm (abs b) by A4, A3, Def2; :: thesis: verum