theorem Th22: :: HILB10_6:22

for i, j, n being Nat
for a being non trivial Nat st 0 < i & i <= n & 0 <= j & j < 4 * n & Px (a,i), Px (a,j) are_congruent_mod Px (a,n) & not j = i holds
j + i = 4 * n