theorem Th21: :: HILB10_6:21

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