let k, n be natural Number ; :: thesis: ( k <= n implies n - k is Element of NAT )
assume A1: k <= n ; :: thesis: n - k is Element of NAT

per cases ( k < n or k = n ) by A1, XXREAL_0:1;

suppose k < n ; :: thesis: n - k is Element of NAT

then k + 1 <= n by Th13;
then consider j being Nat such that
A2: n = (k + 1) + j by Th10;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
n - k = 1 + j by A2;
hence n - k is Element of NAT ; :: thesis: verum

end;

suppose k = n ; :: thesis: n - k is Element of NAT

then n - k = 0 ;
hence n - k is Element of NAT ; :: thesis: verum

end;

end;