let x, y be Integer; :: thesis: (x |^ 2) - (y |^ 3) <> 7
assume A1: (x |^ 2) - (y |^ 3) = 7 ; :: thesis: contradiction
A2: x |^ 2 = x ^2 by WSIERP_1:1;
A3: y |^ 3 = (y * y) * y by POLYEQ_5:2;

per cases ( y is even or y is odd ) ;

suppose y is even ; :: thesis: contradiction

then consider i being Integer such that
A4: y = 2 * i by ABIAN:11;
i |^ 3 = (i * i) * i by POLYEQ_5:2;
then A5: y |^ 3 = (8 * (i |^ 3)) + 0 by A3, A4;
A6: ( (x ^2) mod 8 = 0 or (x ^2) mod 8 = 1 or (x ^2) mod 8 = 4 ) by Th59, Th60;
((x |^ 2) - 7) mod 8 = (((x |^ 2) - 7) + (8 * 1)) mod 8 by NAT_D:61;
then ((x |^ 2) - 7) mod 8 = ((x |^ 2) + 1) mod 8
.= (((x |^ 2) mod 8) + (1 mod 8)) mod 8 by NAT_D:66 ;
then ( ((x |^ 2) - 7) mod 8 = (0 + 1) mod 8 or ((x |^ 2) - 7) mod 8 = (1 + 1) mod 8 or ((x |^ 2) - 7) mod 8 = (4 + 1) mod 8 ) by A2, A6, NAT_D:24;
hence contradiction by A1, A5, NAT_D:24; :: thesis: verum

end;

suppose y is odd ; :: thesis: contradiction

then consider k being Integer such that
A7: y = (2 * k) + 1 by ABIAN:1;
(x |^ 2) + 1 = (y |^ 3) + 8 by A1
.= (y + 2) * (((y - 1) ^2) + 3) by A3 ;
then A8: (4 * (k ^2)) + 3 divides (x |^ 2) + 1 by A7;
ex p, q being Nat st
( p = (4 * q) + 3 & p is prime & p divides (4 * (k ^2)) + 3 ) by NUMBER05:3;
hence contradiction by A2, A8, INT_2:9, Lm18; :: thesis: verum

end;

end;