let r, s be Real; ( frac r < frac s implies frac (r - s) = ((frac r) - (frac s)) + 1 )
assume A1:
frac r < frac s
; frac (r - s) = ((frac r) - (frac s)) + 1
set a = (((r - s) - (frac r)) + (frac s)) - 1;
A2:
(((r - s) - (frac r)) + (frac s)) - 1 = ((r - (frac r)) - (s - (frac s))) - 1
;
A3:
(((r - s) - (frac r)) + (frac s)) - 1 = (r - s) + (((- (frac r)) + (frac s)) - 1)
;
frac s < 1
by INT_1:43;
then A4:
(frac s) - 1 < 1 - 1
by XREAL_1:9;
0 <= frac r
by INT_1:43;
then
((frac s) - 1) - (frac r) <= (frac r) - (frac r)
by A4;
then A5:
(((r - s) - (frac r)) + (frac s)) - 1 <= (r - s) + Q
by A3, XREAL_1:6;
A6:
(((r - s) - (frac r)) + (frac s)) - 1 = ((r - s) - 1) - ((frac r) - (frac s))
;
(frac r) - (frac r) > (frac r) - (frac s)
by A1, XREAL_1:10;
then
((r - s) - 1) - Q < (((r - s) - (frac r)) + (frac s)) - 1
by A6, XREAL_1:10;
then
(((r - s) - (frac r)) + (frac s)) - 1 = [\(r - s)/]
by A5, A2, INT_1:def 6;
hence
frac (r - s) = ((frac r) - (frac s)) + 1
; verum