theorem :: COMPLEX3:103

for a, b being positive heavy Real st log (a,b) > log (b,a) & log (b,a) >= 1 holds
a > b