thus ( i1,i2 are_congruent_mod i3 implies ex i4 being Integer st i3 * i4 = i1 - i2 ) :: thesis: ( ex i4 being Integer st i3 * i4 = i1 - i2 implies i1,i2 are_congruent_mod i3 )

proof

assume i3 divides i1 - i2 ; :: according to INT_1:def 4 :: thesis: ex i4 being Integer st i3 * i4 = i1 - i2
hence ex i4 being Integer st i3 * i4 = i1 - i2 ; :: thesis: verum

end;

given i4 being Integer such that A1: i3 * i4 = i1 - i2 ; :: thesis: i1,i2 are_congruent_mod i3
take i4 ; :: according to INT_1:def 3,INT_1:def 4 :: thesis: i1 - i2 = i3 * i4
thus i1 - i2 = i3 * i4 by A1; :: thesis: verum