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 ) ) ;
then ( a <> 0 & not a is quadratic_residue ) ;
hence Lege_p a = - 1 by Def5; :: thesis: verum

end;

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