theorem Th1: :: INT_8:1

for m being Nat holds RelPrimes m c= Seg m