for n being natural 2 _greater number
for s being non trivial Divisor of n - 1 st s > sqrt n & ex a being natural number st
( a |^ (n - 1),1 are_congruent_mod n & ( for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1 ) ) holds
n is prime