let r, s be Real; :: 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 ;
- (r / s) = (- r) / s by XCMPLX_1:187;
hence - [\(r / s)/] = [\((- r) / s)/] by A1; :: thesis: verum