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