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 x * y = - 2 ; :: thesis: ( ( x = 1 & y = - 2 ) or ( x = 2 & y = - 1 ) or ( x = - 1 & y = 2 ) or ( x = - 2 & y = 1 ) )
then (- x) * y = 2 ;
then ( ( - x = 1 & y = 2 ) or ( - x = 2 & y = 1 ) or ( - x = - 1 & y = - 2 ) or ( - x = - 2 & y = - 1 ) ) by Lm7;
hence ( ( x = 1 & y = - 2 ) or ( x = 2 & y = - 1 ) or ( x = - 1 & y = 2 ) or ( x = - 2 & y = 1 ) ) ; :: thesis: verum