let r, s be Real; :: thesis: ( r / s is not Integer implies - [\(r / s)/] = [\((- r) / s)/] + 1 )
(r / s) - 1 < [\(r / s)/] by Def6;
then - ((r / s) - 1) > - [\(r / s)/] by XREAL_1:24;
then (- (r / s)) + 1 > - [\(r / s)/] ;
then - [\(r / s)/] <= ((- r) / s) + 1 by XCMPLX_1:187;
then A1: (- [\(r / s)/]) - 1 <= (((- r) / s) + 1) - 1 by XREAL_1:9;
assume r / s is not Integer ; :: thesis: - [\(r / s)/] = [\((- r) / s)/] + 1
then [\(r / s)/] < r / s by Th26;
then - (r / s) < - [\(r / s)/] by XREAL_1:24;
then (- (r / s)) - 1 < (- [\(r / s)/]) - 1 by XREAL_1:9;
then ((- r) / s) - 1 < (- [\(r / s)/]) - 1 by XCMPLX_1:187;
then ((- [\(r / s)/]) - 1) + 1 = [\((- r) / s)/] + 1 by A1, Def6;
hence - [\(r / s)/] = [\((- r) / s)/] + 1 ; :: thesis: verum