let n be Nat; :: thesis: ( (2 |^ n) - 1 is prime & (2 |^ n) + 1 is prime implies n = 2 )
assume that
A1: (2 |^ n) - 1 is prime and
A2: (2 |^ n) + 1 is prime ; :: thesis: n = 2

per cases ( n is odd or n is even ) ;

suppose A3: n is odd ; :: thesis: n = 2

3 divides 2 + 1 ;
then 3 divides (2 |^ n) + (1 |^ n) by A3, NEWTON03:25;
then (2 |^ n) + 1 = 3 by A2;
hence n = 2 by A1; :: thesis: verum

end;

suppose n is even ; :: thesis: n = 2

then consider k being Nat such that
A4: n = 2 * k ;

now :: thesis: not n <= 1

assume n <= 1 ; :: thesis: contradiction
then ( n = 0 or n = 1 ) by NAT_1:25;
then 1 - 1 is prime by A1, NEWTON:4;
hence contradiction ; :: thesis: verum

end;

then A5: n is prime by A1, GR_CY_3:28;
2 divides 2 * k ;
hence n = 2 by A4, A5; :: thesis: verum

end;

end;