let k, n be natural Number ; :: thesis: ( k < n implies n - 1 is Element of NAT )
assume k < n ; :: thesis: n - 1 is Element of NAT
then k + 1 <= n by Th13;
then consider j being Nat such that
A1: n = (k + 1) + j by Th10;
n - 1 = k + j by A1;
hence n - 1 is Element of NAT by ORDINAL1:def 12; :: thesis: verum