let a, b be non zero Real; :: thesis: ( a - b = a * b iff (1 / b) - (1 / a) = 1 )
( (1 * a) / (a * b) = 1 / b & (1 * b) / (a * b) = 1 / a ) by XCMPLX_1:91;
then ((1 / b) - (1 / a)) * (a * b) = ((a - b) / (a * b)) * (a * b)
.= a - b by XCMPLX_1:87 ;
hence ( a - b = a * b iff (1 / b) - (1 / a) = 1 ) by XCMPLX_1:7; :: thesis: verum