let r, s be real number ; :: thesis: ( r / s is Integer implies - [\(r / s)/] = [\((- r) / s)/] )
assume r / s is Integer ; :: thesis: - [\(r / s)/] = [\((- r) / s)/]
then A1: [\(r / s)/] = r / s by Th47;
A2: - (r / s) = (- r) / s by XCMPLX_1:187;
then ((- r) / s) - 1 < (- [\(r / s)/]) - 0 by A1, XREAL_1:15;
hence - [\(r / s)/] = [\((- r) / s)/] by A1, A2, Def6; :: thesis: verum