theorem :: NAT_2:28

for k being Nat holds
( not k is trivial iff ( not k is empty & k <> 1 ) ) ;