let r be real number ; :: thesis: for i1, i2 being Integer st r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 holds
i1 = i2
let i1, i2 be Integer; :: thesis: ( r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 implies i1 = i2 )
assume A1: ( r <= i1 & i1 < r + 1 & r <= i2 & i2 < r + 1 ) ; :: thesis: i1 = i2
i2 = i1 + (i2 - i1) ;
then consider i0 being Integer such that
A2: i2 = i1 + i0 ;
A3: ( i0 = 0 implies i2 = i1 ) by A2;

A4: now

assume ( i0 < 0 & i1 <> i2 ) ; :: thesis: contradiction
then i0 <= - 1 by Th21;
then i1 + i0 < (r + 1) + (- 1) by A1, XREAL_1:10;
hence contradiction by A1, A2; :: thesis: verum

end;

now

assume ( 0 < i0 & i1 <> i2 ) ; :: thesis: contradiction
then 1 <= i0 by Lm5;
hence contradiction by A1, A2, XREAL_1:9; :: thesis: verum

end;

hence i1 = i2 by A3, A4; :: thesis: verum