let n be Nat; :: thesis: for a being Integer st n <> 0 holds
a mod n,a are_congruent_mod n
let a be Integer; :: thesis: ( n <> 0 implies a mod n,a are_congruent_mod n )
A1: (a mod n) mod n = a mod n by NAT_D:65;
assume n <> 0 ; :: thesis: a mod n,a are_congruent_mod n
hence a mod n,a are_congruent_mod n by A1, NAT_D:64; :: thesis: verum