let k, n be Nat; for a, b being Integer st k <> 0 & a,b are_congruent_mod n |^ k holds
a,b are_congruent_mod n
let a, b be Integer; ( k <> 0 & a,b are_congruent_mod n |^ k implies a,b are_congruent_mod n )
assume
k <> 0
; ( not a,b are_congruent_mod n |^ k or a,b are_congruent_mod n )
then
n divides n |^ k
by NAT_3:3;
hence
( not a,b are_congruent_mod n |^ k or a,b are_congruent_mod n )
by INT_2:9; verum