theorem :: NAT_2:29

for k being non trivial Nat holds k >= 2