let a, p be Nat; :: thesis: ( p > 1 & (a |^ p) - 1 is Prime implies ( a = 2 & p is Prime ) )
assume that
A1: p > 1 and
A2: (a |^ p) - 1 is Prime ; :: thesis: ( a = 2 & p is Prime )

now

A3: a > 1 by A1, A2, Lm6;
then A4: a >= 1 + 1 by NAT_1:13;
p >= 1 + 1 by A1, NAT_1:13;
then a < a |^ p by A3, PREPOWER:21;
then A5: a - 1 < (a |^ p) - 1 by XREAL_1:11;

now

assume A6: a > 2 ; :: thesis: contradiction
then A7: a - 1 > 2 - 1 by XREAL_1:11;
A8: a - 1 is Element of NAT by A6, NAT_1:20;
a - 1 divides (a |^ p) - 1 by A1, A2, Lm6, Th27;
hence contradiction by A2, A5, A7, A8, NAT_4:12; :: thesis: verum

end;

hence a = 2 by A4, XXREAL_0:1; :: thesis: p is Prime
assume p is not Prime ; :: thesis: contradiction
then consider n being Element of NAT such that
A9: n divides p and
A10: 1 < n and
A11: n < p by A1, NAT_4:12;
consider q being Nat such that
A12: p = n * q by A9, NAT_D:def 3;
1 + 1 <= n by A10, NAT_1:13;
then 2 < 2 |^ n by PREPOWER:21;
then A13: 2 + 1 <= 2 |^ n by NAT_1:13;
2 |^ n <= a |^ n by A4, PREPOWER:17;
then 2 + 1 <= a |^ n by A13, XXREAL_0:2;
then 2 < a |^ n by NAT_1:13;
then A14: 2 - 1 < (a |^ n) - 1 by XREAL_1:11;
a >= 0 + 1 by A1, A2, Lm6;
then A15: (a |^ n) - 1 is Element of NAT by NAT_1:21, PREPOWER:19;
a |^ n < a |^ p by A3, A11, PEPIN:71;
then A16: (a |^ n) - 1 < (a |^ p) - 1 by XREAL_1:11;
(a |^ n) - 1 divides ((a |^ n) |^ q) - 1 by A3, A10, Th27, PEPIN:26;
then (a |^ n) - 1 divides (a |^ p) - 1 by A12, NEWTON:14;
hence contradiction by A2, A16, A15, A14, NAT_4:12; :: thesis: verum

end;

hence ( a = 2 & p is Prime ) ; :: thesis: verum