Parity ((2 * 0) + 1) = 1 by NAT_2:def 1;
hence Parity 1 = 1 ; :: thesis: verum