theorem ABN: :: COMPLEX3:26

for a, b being negative Real holds
( a > b iff 1 / a < 1 / b ) by XREAL_1:119, XREAL_1:99;