let n be non zero Nat; :: thesis: for x being Integer holds
not not x, 0 are_congruent_mod n & ... & not x,n - 1 are_congruent_mod n
let x be Integer; :: thesis: not not x, 0 are_congruent_mod n & ... & not x,n - 1 are_congruent_mod n
x mod n in NAT by INT_1:3, INT_1:57;
then reconsider j = x mod n as Nat ;
(x mod n) + 1 <= n by INT_1:7, INT_1:58;
then A1: ((x mod n) + 1) - 1 <= n - 1 by XREAL_1:9;
take j ; :: thesis: ( 0 <= j & j <= n - 1 & x,j are_congruent_mod n )
thus ( 0 <= j & j <= n - 1 & x,j are_congruent_mod n ) by Th10, A1; :: thesis: verum