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

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 = y ^2 } or a in {[3,3]} )
assume a in { [x,y] where x, y is positive Nat : (2 |^ x) + 1 = y ^2 } ; :: thesis: a in {[3,3]}
then consider x, y being positive Nat such that
A1: a = [x,y] and
A2: (2 |^ x) + 1 = y ^2 ;
A3: (y + 1) * (y - 1) = 2 |^ x by A2;
y - 1 divides (y + 1) * (y - 1) ;
then consider k being Nat such that
A4: y - 1 = 2 |^ k by A2, XPRIMES1:2, NEWTON03:36;
y + 1 divides (y + 1) * (y - 1) ;
then consider s being Nat such that
A5: y + 1 = 2 |^ s by A2, XPRIMES1:2, NEWTON03:36;
y - 1 < y + 1 by XREAL_1:8;
then A6: k < s by A4, A5, PREPOWER:93;
(2 |^ k) * (2 |^ s) = 2 |^ (k + s) by NEWTON:8;
then A7: x = k + s by A3, A4, A5, PEPIN:30;
A8: (2 |^ s) - (2 |^ k) = 2 by A4, A5;

A9: now :: thesis: not k <= 0

assume k <= 0 ; :: thesis: contradiction
then k = 0 ;
then y - 1 = 1 by A4, NEWTON:4;
then 2 |^ s = (2 * 1) + 1 by A5;
hence contradiction by A6; :: thesis: verum

end;

2 |^ k divides 2 |^ s by A6, PEPIN:31;
then A10: 2 |^ k divides 2 |^ 1 by A8, INT_5:1;
then A11: k = 1 by A9, NAT_1:25, PEPIN:31;
2 |^ s = (2 |^ k) + 2 by A4, A5;
then A12: s = 2 by A11, Lm1, PEPIN:30;
y - 1 = 2 by A4, A9, A10, NAT_1:25, PEPIN:31;
hence a in {[3,3]} by A1, A7, A11, A12, TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {[3,3]} or a in { [x,y] where x, y is positive Nat : (2 |^ x) + 1 = y ^2 } )
assume a in {[3,3]} ; :: thesis: a in { [x,y] where x, y is positive Nat : (2 |^ x) + 1 = y ^2 }
then A13: a = [3,3] by TARSKI:def 1;
(2 |^ 3) + 1 = 3 ^2 by Lm2;
hence a in { [x,y] where x, y is positive Nat : (2 |^ x) + 1 = y ^2 } by A13; :: thesis: verum