let i, j be Integer; :: thesis: i gcd j = i gcd (abs j)
set k = i gcd (abs j);
i gcd (abs j) divides abs j by INT_2:def 3;
then consider x being Integer such that
A1: (i gcd (abs j)) * x = abs j by INT_1:def 9;
abs j divides j by Th13;
then consider y being Integer such that
A2: (abs j) * y = j by INT_1:def 9;
A3: for m being Integer st m divides i & m divides j holds
m divides i gcd (abs j)

proof

j divides abs j by Th13;
then consider y being Integer such that
A4: j * y = abs j by INT_1:def 9;
let m be Integer; :: thesis: ( m divides i & m divides j implies m divides i gcd (abs j) )
assume that
A5: m divides i and
A6: m divides j ; :: thesis: m divides i gcd (abs j)
consider x being Integer such that
A7: m * x = j by A6, INT_1:def 9;
m * (x * y) = abs j by A7, A4;
then m divides abs j by INT_1:def 9;
hence m divides i gcd (abs j) by A5, INT_2:def 3; :: thesis: verum

end;

(i gcd (abs j)) * (x * y) = j by A1, A2;
then A8: i gcd (abs j) divides j by INT_1:def 9;
i gcd (abs j) divides i by INT_2:def 3;
hence i gcd j = i gcd (abs j) by A8, A3, INT_2:def 3; :: thesis: verum