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

proof

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

proof

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

end;

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