let x be Integer; :: thesis: ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )
not not x, 0 are_congruent_mod 3 & ... & not x,3 - 1 are_congruent_mod 3 by Th13;
then A1: not not x, 0 are_congruent_mod 3 & ... & not x,2 are_congruent_mod 3 ;

per cases ( x, 0 are_congruent_mod 3 or x,1 are_congruent_mod 3 or x,2 are_congruent_mod 3 ) by A1;

suppose x, 0 are_congruent_mod 3 ; :: thesis: ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )

then x * x,0 * 0 are_congruent_mod 3 by INT_1:18;
hence ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 ) by NEWTON:81; :: thesis: verum

end;

suppose x,1 are_congruent_mod 3 ; :: thesis: ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )

then x * x,1 * 1 are_congruent_mod 3 by INT_1:18;
hence ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 ) by NEWTON:81; :: thesis: verum

end;

suppose x,2 are_congruent_mod 3 ; :: thesis: ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )

then x * x,2 * 2 are_congruent_mod 3 by INT_1:18;
then 4,x * x are_congruent_mod 3 by INT_1:14;
then 4 - 3,x * x are_congruent_mod 3 by INT_1:22;
then x * x,4 - 3 are_congruent_mod 3 by INT_1:14;
hence ( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 ) by NEWTON:81; :: thesis: verum

end;

end;