let a be Integer; :: thesis: for p being Prime holds
( Lege a,p = 1 or Lege a,p = - 1 )
let p be Prime; :: thesis: ( Lege a,p = 1 or Lege a,p = - 1 )

per cases ( a is_quadratic_residue_mod p or not a is_quadratic_residue_mod p ) ;

suppose a is_quadratic_residue_mod p ; :: thesis: ( Lege a,p = 1 or Lege a,p = - 1 )

thus ( Lege a,p = 1 or Lege a,p = - 1 ) by Def3; :: thesis: verum

end;

suppose not a is_quadratic_residue_mod p ; :: thesis: ( Lege a,p = 1 or Lege a,p = - 1 )

thus ( Lege a,p = 1 or Lege a,p = - 1 ) by Def3; :: thesis: verum

end;

end;