theorem Th62: :: NAT_D:62

for n being natural Number st n > 0 holds
for a being Integer holds
( a mod n >= 0 & a mod n < n )