let a, b, c be Integer; :: thesis: ( a,b are_congruent_mod c iff c divides a - b )
thus ( a,b are_congruent_mod c implies c divides a - b ) :: thesis: ( c divides a - b implies a,b are_congruent_mod c )

proof

assume a,b are_congruent_mod c ; :: thesis: c divides a - b
then ex d being Integer st a - b = c * d by INT_1:def 5;
hence c divides a - b by INT_1:def 3; :: thesis: verum

end;

assume c divides a - b ; :: thesis: a,b are_congruent_mod c
then ex d being Integer st a - b = c * d by INT_1:def 3;
hence a,b are_congruent_mod c by INT_1:def 5; :: thesis: verum