for a being Nat
for p being prime Nat st not p divides a holds
ex n being Nat st
( p divides (a |^ n) - 1 & 0 < n & n < p )