theorem :: COMPLEX3:104

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