let i, n be Nat; :: thesis: ( i <= n implies (n - i) + 1 is Element of NAT )
assume i <= n ; :: thesis: (n - i) + 1 is Element of NAT
then reconsider ni = n - i as Element of NAT by INT_1:5;
ni + 1 is Element of NAT ;
hence (n - i) + 1 is Element of NAT ; :: thesis: verum