theorem :: INT_1:13

for i1, i2 being Integer holds i1,i2 are_congruent_mod 1