theorem OPR: :: COMPLEX3:29

for a, b being positive Real holds sgn ((1 / a) - (1 / b)) = sgn (b - a)