let i1, i2 be Integer; :: thesis: for n1, n2 being Element of NAT st i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 holds
n1 <= n2
let n1, n2 be Element of NAT ; :: thesis: ( i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 implies n1 <= n2 )
assume A1: ( i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 ) ; :: thesis: n1 <= n2
then n1 + i1 >= n1 + (- 1) by XREAL_1:8;
then i2 + 1 >= (n1 + (- 1)) + 1 by A1, XREAL_1:8;
hence n1 <= n2 by A1; :: thesis: verum