theorem Th40: :: NAT_6:40

for n being natural Proth number holds
( n is prime iff ex a being natural number st a |^ ((n - 1) / 2), - 1 are_congruent_mod n )