let a, b, r be Real; :: 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 Def6;
then A7: [\r/] <= a by A1, XXREAL_0:2;
A8: [\r/] <= b by A3, A6, 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 A9: ( a < [\r/] + 1 & b >= [\r/] + 1 ) ; :: thesis: a = b
then frac a >= frac r by A1, Th66;
hence a = b by A4, A5, A9, Th69; :: thesis: verum
end;
suppose A10: ( a >= [\r/] + 1 & b < [\r/] + 1 ) ; :: thesis: a = b
then frac a < frac r by A2, Th69;
hence a = b by A3, A5, A10, Th66; :: thesis: verum
end;
suppose A11: ( a < [\r/] + 1 & b < [\r/] + 1 ) ; :: thesis: a = b
then b - 1 < ([\r/] + 1) - 1 by XREAL_1:9;
then A12: [\b/] = [\r/] by A8, Def6;
a - 1 < ([\r/] + 1) - 1 by A11, XREAL_1:9;
then [\a/] = [\r/] by A7, Def6;
hence a = b by A5, A12; :: thesis: verum
end;
suppose ( a >= [\r/] + 1 & b >= [\r/] + 1 ) ; :: thesis: a = b
then ( [\a/] = [\r/] + 1 & [\b/] = [\r/] + 1 ) by A2, A4, Th68;
hence a = b by A5; :: thesis: verum
end;
end;