let r be Real; :: 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 that
A1: i1 <= r and
A2: r - 1 < i1 and
A3: i2 <= r and
A4: r - 1 < i2 ; :: thesis: i1 = i2
i2 = i1 + (i2 - i1) ;
then consider i0 being Integer such that
A5: i2 = i1 + i0 ;

A6: now :: thesis: ( 0 < i0 implies not i1 <> i2 )

assume that
A7: 0 < i0 and
i1 <> i2 ; :: thesis: contradiction
1 <= i0 by A7, Lm4;
then (r - 1) + 1 < i1 + i0 by A2, XREAL_1:8;
hence contradiction by A3, A5; :: thesis: verum

end;

A8: now :: thesis: ( i0 < 0 implies not i1 <> i2 )

assume that
A9: i0 < 0 and
i1 <> i2 ; :: thesis: contradiction
i0 <= - 1 by A9, Th8;
then i1 + i0 <= r + (- 1) by A1, XREAL_1:7;
hence contradiction by A4, A5; :: thesis: verum

end;

( i0 = 0 implies i2 = i1 ) by A5;
hence i1 = i2 by A8, A6; :: thesis: verum