for n, n1, n2 being Nat
for x, y being Integer
for a being non trivial Nat st n1 <= 2 * n & n2 <= 2 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) & not n1,n2 are_congruent_mod 2 * n holds
n1, - n2 are_congruent_mod 2 * n