theorem ABD: :: COMPLEX3:25

for a, b being positive Real holds
( a > b iff 1 / a < 1 / b ) by XREAL_1:118, XREAL_1:76;