Parity a = 2 |^ (2 |-count a) by Def1;
hence not Parity a is zero ; :: thesis: verum