let r, s be real number ; :: thesis: ( 0 <= r & r < s implies [\(r / s)/] = 0 )
assume that
A1: 0 <= r and
A2: r < s ; :: thesis: [\(r / s)/] = 0
A3: 0 <= r / s by A1, A2;
r / s < s / s by A1, A2, XREAL_1:76;
then (r / s) - 1 < (s / s) - 1 by XREAL_1:11;
then (r / s) - 1 < 1 - 1 by A1, A2, XCMPLX_1:60;
hence [\(r / s)/] = 0 by A3, INT_1:def 4; :: thesis: verum