let n, n1, n2 be Nat; :: thesis: for x, y being Integer
for a being non trivial Nat st n1 <= 4 * n & n2 <= 4 * 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
let x, y be Integer; :: thesis: for a being non trivial Nat st n1 <= 4 * n & n2 <= 4 * 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
let a be non trivial Nat; :: thesis: ( n1 <= 4 * n & n2 <= 4 * 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 implies n1, - n2 are_congruent_mod 2 * n )
assume A1: ( n1 <= 4 * n & n2 <= 4 * n & |.x.| = Py (a,n1) & |.y.| = Py (a,n2) & x,y are_congruent_mod Px (a,n) ) ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )
then A2: y,x are_congruent_mod Px (a,n) by INT_1:14;

per cases ( ( n1 <= 2 * n & n2 <= 2 * n ) or ( n1 > 2 * n & n2 > 2 * n ) or ( n1 <= 2 * n & 2 * n < n2 ) or ( n2 <= 2 * n & 2 * n < n1 ) ) ;

suppose ( ( n1 <= 2 * n & n2 <= 2 * n ) or ( n1 > 2 * n & n2 > 2 * n ) or ( n1 <= 2 * n & 2 * n < n2 ) ) ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )

hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by A1, Th34, Lm10, Lm11; :: thesis: verum

end;

suppose ( n2 <= 2 * n & 2 * n < n1 ) ; :: thesis: ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n )

then ( n2,n1 are_congruent_mod 2 * n or n2, - n1 are_congruent_mod 2 * n ) by A1, A2, Lm10;
then ( n1,n2 are_congruent_mod 2 * n or (- 1) * n2,(- 1) * (- n1) are_congruent_mod 2 * n ) by INT_1:14, INT_4:11;
hence ( n1,n2 are_congruent_mod 2 * n or n1, - n2 are_congruent_mod 2 * n ) by INT_1:14; :: thesis: verum

end;

end;