let x, y be Integer; :: thesis: ( not x * y = - 4 or ( x = 1 & y = - 4 ) or ( x = 2 & y = - 2 ) or ( x = 4 & y = - 1 ) or ( x = - 1 & y = 4 ) or ( x = - 2 & y = 2 ) or ( x = - 4 & y = 1 ) )
assume x * y = - 4 ; :: thesis: ( ( x = 1 & y = - 4 ) or ( x = 2 & y = - 2 ) or ( x = 4 & y = - 1 ) or ( x = - 1 & y = 4 ) or ( x = - 2 & y = 2 ) or ( x = - 4 & y = 1 ) )
then (- x) * y = 4 ;
then ( ( - x = 1 & y = 4 ) or ( - x = 2 & y = 2 ) or ( - x = 4 & y = 1 ) or ( - x = - 1 & y = - 4 ) or ( - x = - 2 & y = - 2 ) or ( - x = - 4 & y = - 1 ) ) by Lm5;
hence ( ( x = 1 & y = - 4 ) or ( x = 2 & y = - 2 ) or ( x = 4 & y = - 1 ) or ( x = - 1 & y = 4 ) or ( x = - 2 & y = 2 ) or ( x = - 4 & y = 1 ) ) ; :: thesis: verum