theorem AM2: :: COMPLEX3:100

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