let n, i be Nat; :: thesis: ( i <= n implies i + 1 is Nat of n )
assume i <= n ; :: thesis: i + 1 is Nat of n
then A1: i + 1 <= n + 1 by XREAL_1:7;
1 <= i + 1 by NAT_1:11;
hence i + 1 is Nat of n by A1, Def2; :: thesis: verum