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