theorem Th28: :: GR_CY_3:28

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