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