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