let r, a, b be real number ; :: thesis: ( r <= a & a < r + 1 & r <= b & b < r + 1 & frac a = frac b implies a = b )
assume that
A1: r <= a and
A2: a < r + 1 and
A3: r <= b and
A4: b < r + 1 and
A5: frac a = frac b ; :: thesis: a = b
A6: frac a = a - [\a/] by INT_1:def 6;
A7: frac b = b - [\b/] by INT_1:def 6;
[\r/] <= r by INT_1:def 4;
then A8: ( [\r/] <= a & [\r/] <= b ) by A1, A3, XXREAL_0:2;

per cases ( ( a < [\r/] + 1 & b >= [\r/] + 1 ) or ( a >= [\r/] + 1 & b < [\r/] + 1 ) or ( a < [\r/] + 1 & b < [\r/] + 1 ) or ( a >= [\r/] + 1 & b >= [\r/] + 1 ) ) ;

suppose ( a < [\r/] + 1 & b >= [\r/] + 1 ) ; :: thesis: a = b

then ( frac a >= frac r & frac b < frac r ) by A1, A4, Th3, Th6;
hence a = b by A5; :: thesis: verum

end;

suppose ( a >= [\r/] + 1 & b < [\r/] + 1 ) ; :: thesis: a = b

then ( frac a < frac r & frac b >= frac r ) by A2, A3, Th3, Th6;
hence a = b by A5; :: thesis: verum

end;

suppose ( a < [\r/] + 1 & b < [\r/] + 1 ) ; :: thesis: a = b

then ( a - 1 < ([\r/] + 1) - 1 & b - 1 < ([\r/] + 1) - 1 ) by XREAL_1:11;
then ( [\a/] = [\r/] & [\b/] = [\r/] ) by A8, INT_1:def 4;
hence a = b by A5, A6, A7; :: thesis: verum

end;

suppose ( a >= [\r/] + 1 & b >= [\r/] + 1 ) ; :: thesis: a = b

then ( [\a/] = [\r/] + 1 & [\b/] = [\r/] + 1 ) by A2, A4, Th5;
hence a = b by A5, A6, A7; :: thesis: verum

end;

end;