:: deftheorem defines RelPrimes INT_8:def 1 :
for m being Nat holds RelPrimes m = { k where k is Element of NAT : ( m,k are_coprime & 1 <= k & k <= m ) } ;