theorem Th10: :: NAT_6:10

for i being Integer
for j being non zero Integer holds i,i mod j are_congruent_mod j