set A = { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } ;
set B = { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } ;
{ [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } = { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 }

proof

thus { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } c= { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } :: according to XBOOLE_0:def 10 :: thesis: { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } c= { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } or a in { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } )
assume a in { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } ; :: thesis: a in { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 }
then consider x, y being positive Nat such that
A1: ( a = [x,y] & ((x + 1) |^ 3) - (x |^ 3) = y ^2 ) ;
(((x + 1) |^ 3) - (x |^ 3)) - (y ^2) = (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 by Lm13;
hence a in { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } by A1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } or a in { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } )
assume a in { [x,y] where x, y is positive Nat : (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 } ; :: thesis: a in { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 }
then consider x, y being positive Nat such that
A2: ( a = [x,y] & (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 = 0 ) ;
(((x + 1) |^ 3) - (x |^ 3)) - (y ^2) = (((3 * (x ^2)) + (3 * x)) - (y ^2)) + 1 by Lm13;
hence a in { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } by A2; :: thesis: verum

end;

hence { [x,y] where x, y is positive Nat : ((x + 1) |^ 3) - (x |^ 3) = y ^2 } is infinite by Th57; :: thesis: verum