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= {[1,1]} :: according to XBOOLE_0:def 10 :: thesis: {[1,1]} 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 {[1,1]} )
assume a in { [x,y] where x, y is positive Nat : (2 |^ x) - 1 = y ^2 } ; :: thesis: a in {[1,1]}
then consider x, y being positive Nat such that
A1: a = [x,y] and
A2: (2 |^ x) - 1 = y ^2 ;

per cases ( x > 1 or x <= 1 ) ;

suppose x > 1 ; :: thesis: a in {[1,1]}

then x >= 1 + 1 by NAT_1:13;
then consider k being positive Nat such that
A3: (2 |^ x) - 1 = (4 * k) - 1 by NUMBER09:11;
A4: ( (y ^2) mod 4 = 0 or (y ^2) mod 4 = 1 ) by PYTHTRIP:3, PYTHTRIP:4;
((4 * k) - 1) mod 4 = ((((4 * k) + 0) mod 4) - (1 mod 4)) mod 4 by INT_6:7
.= (3 + ((- 1) * 4)) mod 4 by NAT_D:24
.= 3 mod 4 by NAT_D:61 ;
hence a in {[1,1]} by A2, A3, A4, NAT_D:24; :: thesis: verum

end;

suppose x <= 1 ; :: thesis: a in {[1,1]}

then A5: x = 1 by NAT_1:25;
then y = 1 by A2, NAT_1:15;
hence a in {[1,1]} by A1, A5, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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