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: [\r/] <= r by INT_1:def 4;
then A7: [\r/] <= a by A1, XXREAL_0:2;
A8: [\r/] <= b by A3, A6, XXREAL_0:2;
A9: ( frac a = a - [\a/] & frac b = b - [\b/] ) by INT_1:def 6;

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 A10: ( a < [\r/] + 1 & b >= [\r/] + 1 ) ; :: thesis: a = b

then frac a >= frac r by A1, Th3;
hence a = b by A4, A5, A10, Th6; :: thesis: verum

end;

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

then frac a < frac r by A2, Th6;
hence a = b by A3, A5, A11, Th3; :: thesis: verum

end;

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

then b - 1 < ([\r/] + 1) - 1 by XREAL_1:11;
then A13: [\b/] = [\r/] by A8, INT_1:def 4;
a - 1 < ([\r/] + 1) - 1 by A12, XREAL_1:11;
then [\a/] = [\r/] by A7, INT_1:def 4;
hence a = b by A5, A9, A13; :: 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, A9; :: thesis: verum

end;

end;