let m, n be Nat; :: thesis: ( m < n implies ex p being Element of NAT st
( n = m + p & 1 <= p ) )
assume A1: m < n ; :: thesis: ex p being Element of NAT st
( n = m + p & 1 <= p )
then consider p being Nat such that
A2: n = m + p by NAT_1:10;
reconsider p = p as Element of NAT by ORDINAL1:def 12;
take p ; :: thesis: ( n = m + p & 1 <= p )
thus n = m + p by A2; :: thesis: 1 <= p
assume p < 1 ; :: thesis: contradiction
then p < 0 + 1 ;
then p = 0 by NAT_1:13;
hence contradiction by A1, A2; :: thesis: verum