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