n + 1 > 0 + 1 by XREAL_1:6;
then n >= 1 by NAT_1:13;
then n - 1 >= 1 - 1 by XREAL_1:9;
then n - 1 in NAT by INT_1:3;
hence n - 1 is natural ; :: thesis: verum