( a mod 2 = 0 * 0 or a mod 2 = 1 * 1 ) by NAT_D:12;
hence a mod 2 is square ; :: thesis: verum