let k, n be Nat; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } iff ( n is prime & k in Segm n & not k in {0} ) )
set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;
thus ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } implies ( n is prime & k in Segm n & not k in {0} ) ) :: thesis: ( n is prime & k in Segm n & not k in {0} implies ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & 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_coprime & kk >= 1 & kk <= n ) } ; :: thesis: ( n is prime & k in Segm n & not k in {0} )
A3: ex kk being Element of NAT st
( kk = k & n,kk are_coprime & kk >= 1 & kk <= n ) by A2;
then k <> n by A1, Lm2, Th1;
then k < n by A3, XXREAL_0:1;
hence ( n is prime & k in Segm n & not k in {0} ) by A1, A3, NAT_1:44, TARSKI:def 1; :: thesis: verum

end;

assume that
A4: n is prime and
A5: k in Segm n and
A6: not k in {0} ; :: thesis: ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & 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:44;
then ( k in NAT & k,n are_coprime ) by A4, A7, Th2, ORDINAL1:def 12;
hence ( n is prime & k in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ) by A4, A9, A8; :: thesis: verum