theorem AG1: :: COMPLEX3:97

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