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