let i1, i2, i3, i5 be Integer; :: thesis: ( i1 + i2,i3 are_congruent_mod i5 iff i1,i3 - i2 are_congruent_mod i5 )
thus ( i1 + i2,i3 are_congruent_mod i5 implies i1,i3 - i2 are_congruent_mod i5 ) :: thesis: ( i1,i3 - i2 are_congruent_mod i5 implies i1 + i2,i3 are_congruent_mod i5 )

proof

assume i1 + i2,i3 are_congruent_mod i5 ; :: thesis: i1,i3 - i2 are_congruent_mod i5
then A1: ex i0 being Integer st i5 * i0 = (i1 + i2) - i3 by Def3;
(i1 + i2) - i3 = i1 - (i3 - i2) ;
hence i1,i3 - i2 are_congruent_mod i5 by A1, Def3; :: thesis: verum

end;

assume i1,i3 - i2 are_congruent_mod i5 ; :: thesis: i1 + i2,i3 are_congruent_mod i5
then A2: ex i0 being Integer st i5 * i0 = i1 - (i3 - i2) by Def3;
i1 - (i3 - i2) = (i1 + i2) - i3 ;
hence i1 + i2,i3 are_congruent_mod i5 by A2, Def3; :: thesis: verum