let n be Nat; :: thesis: for a being Integer st n <> 0 holds
ex an being Nat st an,a are_congruent_mod n
let a be Integer; :: thesis: ( n <> 0 implies ex an being Nat st an,a are_congruent_mod n )
assume A1: n <> 0 ; :: thesis: ex an being Nat st an,a are_congruent_mod n
reconsider an = a mod n as Element of NAT by INT_1:3, INT_1:57;
take an ; :: thesis: an,a are_congruent_mod n
thus an,a are_congruent_mod n by A1, Lm7; :: thesis: verum