let p be Prime; :: thesis: Lege 1,p = 1
1 gcd p = 1 by WSIERP_1:13;
then Lege (1 ^2 ),p = 1 by Th26;
hence Lege 1,p = 1 ; :: thesis: verum