for a, p being Nat st p > 1 & (a |^ p) - 1 is Prime holds
( a = 2 & p is Prime )