theorem :: COMPLEX3:27

for a, b being positive Real holds
( 1 / a > 1 / b iff - a > - b ) by ABD, XREAL_1:24;