set S = { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } ;
thus { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } c= {3} :: according to XBOOLE_0:def 10 :: thesis: {3} c= { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } or x in {3} )
assume x in { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } ; :: thesis: x in {3}
then consider n being Nat such that
A1: x = n and
A2: n divides (2 |^ n) + 1 and
A3: n is prime ;
A4: ((2 |^ n) + 1) mod n = 0 by A2, A3, INT_1:62;
A5: n <> 2 by A2;
1 + 1 <= n by A3, NAT_1:13;
then 2 < n by A5, XXREAL_0:1;
then A6: 2 mod n = 2 by NAT_D:24;
A7: (2 |^ n) mod n = 2 mod n by A3, EULER_2:19;
A8: (((2 |^ n) + 1) - (2 |^ n)) mod n = ((((2 |^ n) + 1) mod n) - ((2 |^ n) mod n)) mod n by INT_6:7;
(1 - (- 2)) mod n = ((1 mod n) - ((- 2) mod n)) mod n by INT_6:7;
then n divides 3 by A3, A4, A7, A6, A8, INT_1:62;
then n = 3 by A3, PEPIN:41;
hence x in {3} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {3} or x in { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } )
assume x in {3} ; :: thesis: x in { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) }
then A9: x = 3 by TARSKI:def 1;
3 |^ 1 divides (2 |^ (3 |^ 1)) + 1 by Th37;
hence x in { n where n is Nat : ( n divides (2 |^ n) + 1 & n is prime ) } by A9, PEPIN:41; :: thesis: verum