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