let x, y be integer number ; :: thesis: for n being integer positive number holds
( x,y are_congruent_mod n iff x mod n = y mod n )
let n be integer positive number ; :: thesis: ( x,y are_congruent_mod n iff x mod n = y mod n )

A1: now :: thesis: ( x,y are_congruent_mod n implies x mod n = y mod n )

assume x,y are_congruent_mod n ; :: thesis: x mod n = y mod n
then consider k being Integer such that
A2: x = (k * n) + y by Th9;
thus x mod n = y mod n by A2, EULER_1:12; :: thesis: verum

end;

now :: thesis: ( x mod n = y mod n implies x,y are_congruent_mod n )

assume A3: x mod n = y mod n ; :: thesis: x,y are_congruent_mod n
A4: x,x mod n are_congruent_mod n by Th10;
y mod n,y are_congruent_mod n by Th10, INT_1:14;
hence x,y are_congruent_mod n by A3, A4, INT_1:15; :: thesis: verum

end;

hence ( x,y are_congruent_mod n iff x mod n = y mod n ) by A1; :: thesis: verum