theorem Th2: :: POLYFORM:3

for k being Integer st 1 <= k holds
k is Nat