let n, a, b be Integer; :: thesis: ( ( n <> 0 & a mod n = b mod n implies a,b are_congruent_mod n ) & ( a,b are_congruent_mod n implies a mod n = b mod n ) )

hereby :: thesis: ( a,b are_congruent_mod n implies a mod n = b mod n )

assume A1: n <> 0 ; :: thesis: ( a mod n = b mod n implies a,b are_congruent_mod n )
assume a mod n = b mod n ; :: thesis: a,b are_congruent_mod n
then a - ((a div n) * n) = b mod n by A1, INT_1:def 10;
then a - ((a div n) * n) = b - ((b div n) * n) by A1, INT_1:def 10;
then a - b = ((- (b div n)) + (a div n)) * n ;
then n divides a - b by INT_1:def 3;
hence a,b are_congruent_mod n by INT_2:15; :: thesis: verum

end;

assume a,b are_congruent_mod n ; :: thesis: a mod n = b mod n
then n divides a - b by INT_2:15;
then consider k being Integer such that
A2: n * k = a - b by INT_1:def 3;
a = (n * k) + b by A2;
hence a mod n = b mod n by Th61; :: thesis: verum