let x, y, n be integer number ; :: thesis: ( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y )
now :: thesis: ( x,y are_congruent_mod n implies ex k being Integer st x = (k * n) + y )
assume x,y are_congruent_mod n ; :: thesis: ex k being Integer st x = (k * n) + y
then consider k being integer Number such that
A1: n * k = x - y ;
x = (n * k) + y by A1;
hence ex k being Integer st x = (k * n) + y ; :: thesis: verum
end;
hence ( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y ) ; :: thesis: verum