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