( not 2 is trivial & 2 divides a ) by ABIAN:def 1;
then 2 |-count a >= 1 by NAT_1:14, NEWTON03:89;
then ( 2 |^ (2 |-count a) >= 2 |^ 1 & 1 + 1 > 1 + 0 ) by PREPOWER:12;
then 2 |^ (2 |-count a) > 1 by XXREAL_0:2;
hence not Parity a is trivial by Def1; :: thesis: verum