let x, y be Integer; :: thesis: ( not x * y = 2 or ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) )
assume A1: x * y = 2 ; :: thesis: ( ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) )
A2: x divides x * y ;

per cases ( x >= 0 or x < 0 ) ;

suppose x >= 0 ; :: thesis: ( ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) )

then x in NAT by INT_1:3;
then ( x = 1 or x = 2 ) by A1, A2, XPRIMES1:2;
hence ( ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) ) by A1; :: thesis: verum

end;

suppose x < 0 ; :: thesis: ( ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) )

then - x in NAT by INT_1:3;
then ( - x = 1 or - x = 2 ) by A1, A2, INT_2:10, XPRIMES1:2;
then ( x = - 1 or x = - 2 ) ;
hence ( ( x = 1 & y = 2 ) or ( x = 2 & y = 1 ) or ( x = - 1 & y = - 2 ) or ( x = - 2 & y = - 1 ) ) by A1; :: thesis: verum

end;

end;