let a be Real; :: thesis: for b being positive Real holds - [\(a / (- b))/] >= [\(a / b)/]
let b be positive Real; :: thesis: - [\(a / (- b))/] >= [\(a / b)/]
- [\(a / (- b))/] = - [\(- (a / b))/] by XCMPLX_1:188
.= [/(a / b)\] by FCB ;
hence - [\(a / (- b))/] >= [\(a / b)/] by INT_1:34, INT_1:35; :: thesis: verum