for k, n being Nat holds
( 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} ) )