let i1, i2, i5, i3 be Integer; :: thesis: ( i1,i2 are_congruent_mod i5 & i2,i3 are_congruent_mod i5 implies i1,i3 are_congruent_mod i5 )
assume that
A1: i1,i2 are_congruent_mod i5 and
A2: i2,i3 are_congruent_mod i5 ; :: thesis: i1,i3 are_congruent_mod i5
consider i8 being Integer such that
A3: i5 * i8 = i1 - i2 by A1, Def3;
consider i9 being Integer such that
A4: i5 * i9 = i2 - i3 by A2, Def3;
i5 * (i8 + i9) = i1 - i3 by A3, A4;
hence i1,i3 are_congruent_mod i5 by Def3; :: thesis: verum