let i1, i2, i5, i3 be Integer; :: thesis: ( i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 implies i2,i3 are_congruent_mod i5 )
assume ( i1,i2 are_congruent_mod i5 & i1,i3 are_congruent_mod i5 ) ; :: thesis: i2,i3 are_congruent_mod i5
then A1: ( i2,i1 are_congruent_mod i5 & i3,i1 are_congruent_mod i5 ) by INT_1:35;
then consider t1 being Integer such that
A2: i5 * t1 = i2 - i1 by INT_1:def 3;
consider t2 being Integer such that
A3: i5 * t2 = i3 - i1 by A1, INT_1:def 3;
i2 - i3 = i5 * (t1 - t2) by A2, A3;
hence i2,i3 are_congruent_mod i5 by INT_1:def 3; :: thesis: verum