let n, k be Nat; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } iff ( n is prime & k in n & not k in {0 } ) )
set X = { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ;
thus ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } implies ( n is prime & k in n & not k in {0 } ) ) :: thesis: ( n is prime & k in n & not k in {0 } implies ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ) )

proof

assume that
A1: n is prime and
A2: k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ; :: thesis: ( n is prime & k in n & not k in {0 } )
A3: ex kk being Element of NAT st
( kk = k & n,kk are_relative_prime & kk >= 1 & kk <= n ) by A2;
then k <> n by A1, Lm2, Th2;
then k < n by A3, XXREAL_0:1;
hence ( n is prime & k in n & not k in {0 } ) by A1, A3, NAT_1:45, TARSKI:def 1; :: thesis: verum

end;

assume that
A4: n is prime and
A5: k in n and
A6: not k in {0 } ; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } )
A7: k <> 0 by A6, TARSKI:def 1;
then A8: k >= 1 by NAT_1:14;
A9: k < n by A5, NAT_1:45;
then ( k in NAT & k,n are_relative_prime ) by A4, A7, Th3, ORDINAL1:def 13;
hence ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_relative_prime & kk >= 1 & kk <= n ) } ) by A4, A9, A8; :: thesis: verum