for n being Nat holds 1 is Nat of n