let n be non zero Nat; :: thesis: for x being Integer
for k, l being Nat st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds
k = l
let x be Integer; :: thesis: for k, l being Nat st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds
k = l
let k, l be Nat; :: thesis: ( k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n implies k = l )
assume A1: ( k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n ) ; :: thesis: k = l
hence k = x mod n by Th12
.= l by A1, Th12 ;
:: thesis: verum