a |^ (parity a) = 1 * (a |^ 0) ;
hence ( a |^ (parity a) is trivial & not a |^ (parity a) is zero ) by NAT_2:def 1; :: thesis: verum