k + 2 <> 1 by NAT_1:12;
hence ( not k + 2 is trivial & not k + 2 is zero ) by NAT_2:def 1; :: thesis: verum