1 ^2 is_quadratic_residue_mod 2 by Th9;
hence 1 is_quadratic_residue_mod 2 ; :: thesis: verum