theorem :: INT_8:2

for m being Nat st 1 <= m holds
RelPrimes m <> {}