2 |-count (a + 1) = 0 ;
then Parity (a + 1) = 1 * (2 |^ 0) by Def1;
hence not Parity (a + 1) is even ; :: thesis: verum