theorem AG2: :: COMPLEX3:99

for a being positive heavy Real
for b being positive Real holds
( a < b iff log (a,b) > 1 )