let a, b be negative Real; :: thesis: sgn ((1 / a) - (1 / b)) = sgn (b - a)
A1: sgn (a * b) = 1 by ABSVALUE:def 2;
( ((1 / a) * a) * b = (1 / a) * (a * b) & (1 / b) * (a * b) = ((1 / b) * b) * a & (1 / b) * b = 1 & (1 / a) * a = 1 ) by XCMPLX_1:87;
then ( (1 / a) * (a * b) = b & (1 / b) * (a * b) = a ) ;
then sgn (b - a) = sgn (((1 / a) - (1 / b)) * (a * b))
.= (sgn ((1 / a) - (1 / b))) * (sgn (a * b)) by ABSVALUE:18 ;
hence sgn ((1 / a) - (1 / b)) = sgn (b - a) by A1; :: thesis: verum