theorem :: INT_1:20

for i1, i2, i3, i4, i5 being Integer st i4 * i5 = i3 & i1,i2 are_congruent_mod i3 holds
i1,i2 are_congruent_mod i4