theorem Th10: :: NAT_6:10

for i being integer number
for j being non zero integer number holds i,i mod j are_congruent_mod j