theorem Th21: :: MIDSP_3:21

for n being Nat holds 1 is Nat of n