let p be Prime; :: thesis: for a being Integer holds
( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 )
let a be Integer; :: thesis: ( Leg (a,p) = 1 or Leg (a,p) = 0 or Leg (a,p) = - 1 )
assume A1: ( Leg (a,p) <> 1 & Leg (a,p) <> 0 ) ; :: thesis: Leg (a,p) = - 1
a gcd p = 1

proof

( a gcd p = 1 or a gcd p = p ) by INT_2:def 4, INT_2:21;
hence a gcd p = 1 by A1, Def4, INT_2:21; :: thesis: verum

end;

hence Leg (a,p) = - 1 by A1, Def4; :: thesis: verum