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