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