let k be Nat; :: thesis: for i1, i2 being Integer st i1 + k = i2 holds
i1 <= i2
let i1, i2 be Integer; :: thesis: ( i1 + k = i2 implies i1 <= i2 )
reconsider i0 = k as Integer ;
assume i1 + k = i2 ; :: thesis: i1 <= i2
then 0 + (i1 + k) <= k + i2 by XREAL_1:6;
then (i1 + i0) - i0 <= (i2 + i0) - i0 by XREAL_1:9;
hence i1 <= i2 ; :: thesis: verum