theorem Th22: :: INT_8:22

for m being Nat holds RelPrimes m is_RRS_of m