theorem ADB: :: COMPLEX3:77

for a, b being positive heavy Real holds
( (a + b) - 1 > a / b & a / b > 1 / ((a + b) - 1) )