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

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

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

then x in NAT by INT_1:3;
then x in {1,2,4,8} by A1, A2, NUMBER03:12;
then ( x = 1 or x = 2 or x = 4 or x = 8 ) by ENUMSET1:def 2;
hence ( ( x = 1 & y = 8 ) or ( x = 2 & y = 4 ) or ( x = 4 & y = 2 ) or ( x = 8 & y = 1 ) or ( x = - 1 & y = - 8 ) or ( x = - 2 & y = - 4 ) or ( x = - 4 & y = - 2 ) or ( x = - 8 & y = - 1 ) ) by A1; :: thesis: verum

end;

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

then - x in NAT by INT_1:3;
then - x in {1,2,4,8} by A1, A2, INT_2:10, NUMBER03:12;
then ( - x = 1 or - x = 2 or - x = 4 or - x = 8 ) by ENUMSET1:def 2;
then ( x = - 1 or x = - 2 or x = - 4 or x = - 8 ) ;
hence ( ( x = 1 & y = 8 ) or ( x = 2 & y = 4 ) or ( x = 4 & y = 2 ) or ( x = 8 & y = 1 ) or ( x = - 1 & y = - 8 ) or ( x = - 2 & y = - 4 ) or ( x = - 4 & y = - 2 ) or ( x = - 8 & y = - 1 ) ) by A1; :: thesis: verum

end;

end;