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

proof

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

end;

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