let i1, i2, i3, i4, i5 be Integer; :: thesis: ( i4 * i5 = i3 & i1,i2 are_congruent_mod i3 implies i1,i2 are_congruent_mod i4 )
assume A1: i4 * i5 = i3 ; :: thesis: ( not i1,i2 are_congruent_mod i3 or i1,i2 are_congruent_mod i4 )
assume i1,i2 are_congruent_mod i3 ; :: thesis: i1,i2 are_congruent_mod i4
then consider i0 being Integer such that
A2: i3 * i0 = i1 - i2 ;
i1 - i2 = i4 * (i5 * i0) by A1, A2;
hence i1,i2 are_congruent_mod i4 ; :: thesis: verum