let a, b be Integer; :: thesis: a gcd b = (abs a) gcd (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: ( m divides abs a & m divides abs b implies m divides a gcd b )
assume ( m divides abs a & m divides abs b ) ; :: thesis: m divides a gcd b
then ( m divides a & m divides b ) by A2, A1, Th14;
hence m divides a gcd b by Def3; :: thesis: verum

end;

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