let r be real number ; :: thesis: for i1, i2 being Integer st i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 holds
i1 = i2
let i1, i2 be Integer; :: thesis: ( i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 implies i1 = i2 )
assume A1: ( i1 <= r & r - 1 < i1 & i2 <= r & r - 1 < i2 ) ; :: 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) by A1, XREAL_1:9;
hence contradiction by A1, A2; :: thesis: verum

end;

now

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

end;

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