let k, i be Integer; :: thesis: ( k < i implies ex j being Element of NAT st
( j = i - k & 1 <= j ) )
assume k < i ; :: thesis: ex j being Element of NAT st
( j = i - k & 1 <= j )
then A1: k - k < i - k by XREAL_1:9;
then reconsider j = i - k as Element of NAT by Th3;
reconsider j9 = j, Z9 = 0 as Integer ;
take j ; :: thesis: ( j = i - k & 1 <= j )
thus j = i - k ; :: thesis: 1 <= j
Z9 + 1 <= j9 by A1, Th7;
hence 1 <= j ; :: thesis: verum