n >= m by EC_PF_2:def 1;
then reconsider nn = n - 1 as Element of NAT by INT_1:3;
n - 1 >= m - 1 by EC_PF_2:def 1, XREAL_1:9;
then n - 1 in NAT by INT_1:3;
hence n - 1 is natural ; :: thesis: verum