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

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 3;
hence c divides a - b by INT_1:def 9; :: thesis: verum

end;

( c divides a - b implies a,b are_congruent_mod c )

proof

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 9;
hence a,b are_congruent_mod c by INT_1:def 3; :: thesis: verum

end;

hence ( a,b are_congruent_mod c iff c divides a - b ) by A1; :: thesis: verum