now :: thesis: for x being integer number holds not x |^ 2,2 are_congruent_mod 3
assume ex x being integer number st x |^ 2,2 are_congruent_mod 3 ; :: thesis: contradiction
then consider x being integer number such that
A1: x |^ 2,2 are_congruent_mod 3 ;
now :: thesis: ( ( x |^ 2, 0 are_congruent_mod 3 & contradiction ) or ( x |^ 2,1 are_congruent_mod 3 & contradiction ) )
end;
hence contradiction ; :: thesis: verum
end;
hence 2 is_quadratic_non_residue_mod 3 by Th22; :: thesis: verum