let r, s be Real; :: thesis: ( r >= s implies ( [\r/] >= [\s/] & [/r\] >= [/s\] ) )
assume A1: r >= s ; :: thesis: ( [\r/] >= [\s/] & [/r\] >= [/s\] )
A2: ( [\r/] <= r & r - 1 < [\r/] & [\s/] <= s & s - 1 < [\s/] ) by INT_1:def 6;
A3: ( [/r\] >= r & r + 1 > [/r\] & [/s\] >= s & s + 1 > [/s\] ) by INT_1:def 7;
assume ( not [\r/] >= [\s/] or not [/r\] >= [/s\] ) ; :: thesis: contradiction

per cases then ( [\r/] < [\s/] or [/r\] < [/s\] ) ;

suppose [\r/] < [\s/] ; :: thesis: contradiction

then B2: [\r/] + 1 <= [\s/] by INT_1:7;
(r - 1) + 1 < [\r/] + 1 by A2, XREAL_1:6;
then ( r < [\s/] & [\s/] <= s ) by INT_1:def 6, B2, XXREAL_0:2;
hence contradiction by A1, XXREAL_0:2; :: thesis: verum

end;

suppose [/r\] < [/s\] ; :: thesis: contradiction

then B2: [/r\] + 1 <= [/s\] by INT_1:7;
r + 1 <= [/r\] + 1 by A3, XREAL_1:6;
then ( r + 1 <= [/s\] & [/s\] < s + 1 ) by B2, INT_1:def 7, XXREAL_0:2;
then r + 1 < s + 1 by XXREAL_0:2;
hence contradiction by A1, XREAL_1:6; :: thesis: verum

end;

end;