let n, m be Element of NAT ; :: thesis: ( n < m implies ex k being Element of NAT st m = (n + 1) + k )
assume A1: n < m ; :: thesis: ex k being Element of NAT st m = (n + 1) + k
then consider k1 being Nat such that
A2: m = n + k1 by NAT_1:10;
k1 <> 0 by A1, A2;
then consider n1 being Nat such that
A3: k1 = n1 + 1 by NAT_1:6;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 13;
take k = n1; :: thesis: m = (n + 1) + k
thus m = (n + 1) + k by A2, A3; :: thesis: verum