let p be Prime; :: thesis: for a being Element of (GF p) holds
( a is not_quadratic_residue iff Lege_p a = - 1 )
let a be Element of (GF p); :: thesis: ( a is not_quadratic_residue iff Lege_p a = - 1 )

hereby :: thesis: ( Lege_p a = - 1 implies a is not_quadratic_residue )

assume a is not_quadratic_residue ; :: thesis: Lege_p a = - 1
then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by QRDef2;
then ( a <> 0 & not a is quadratic_residue ) by QRDef1;
hence Lege_p a = - 1 by QRDef3; :: thesis: verum

end;

assume Lege_p a = - 1 ; :: thesis: a is not_quadratic_residue
then ( a <> 0 & not a is quadratic_residue ) by QRDef3;
then ( a <> 0 & ( for x being Element of (GF p) holds not x |^ 2 = a ) ) by QRDef1;
hence a is not_quadratic_residue by QRDef2; :: thesis: verum