for m being Nat holds RelPrimes m c= Seg m