theorem Th5: :: EULER_2:5

for m, n being Nat holds (m mod n) mod n = m mod n