( a mod 2 = 0 or a mod 2 = 1 ) by NAT_1:23, INT_1:58;
hence a mod 2 is trivial Nat by NAT_2:def 1; :: thesis: verum