theorem Th33: :: EC_PF_1:33

for p being Prime
for a being Element of (GF p) holds
( a is quadratic_residue iff Lege_p a = 1 ) by Def5;