let p be Prime; :: thesis: Lege (1,p) = 1
1 < p by INT_2:def 4;
then 1 mod p <> 0 by NAT_D:14;
then Lege ((1 ^2),p) = 1 by Th26;
hence Lege (1,p) = 1 ; :: thesis: verum