let r be Real; :: 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 that
A1: r <= i1 and
A2: i1 < r + 1 and
A3: r <= i2 and
A4: i2 < r + 1 ; :: thesis: i1 = i2
i2 = i1 + (i2 - i1) ;
then consider i0 being Integer such that
A5: i2 = i1 + i0 ;
A6: now :: thesis: ( i0 < 0 implies not i1 <> i2 )
assume that
A7: i0 < 0 and
i1 <> i2 ; :: thesis: contradiction
i0 <= - 1 by A7, Th8;
then i1 + i0 < (r + 1) + (- 1) by A2, XREAL_1:8;
hence contradiction by A3, A5; :: thesis: verum
end;
A8: now :: thesis: ( 0 < i0 implies not i1 <> i2 )
assume that
A9: 0 < i0 and
i1 <> i2 ; :: thesis: contradiction
1 <= i0 by A9, Lm4;
hence contradiction by A1, A4, A5, XREAL_1:7; :: thesis: verum
end;
( i0 = 0 implies i2 = i1 ) by A5;
hence i1 = i2 by A6, A8; :: thesis: verum