for m being Nat holds RelPrimes m is_RRS_of m