( a = 0 or a = 1 ) by NAT_2:def 1;
hence ( a ! is trivial & not a ! is zero ) by NAT_2:def 1, NEWTON:12, NEWTON:13; :: thesis: verum