for k being non trivial Nat holds k >= 2