theorem Th28: :: INT_5:28

for a being Integer
for p being Prime st p > 2 & a gcd p = 1 holds
Lege (a,p),a |^ ((p -' 1) div 2) are_congruent_mod p