theorem :: COMPLEX3:112

for a being positive light Real
for c being positive heavy Real
for b, d being positive Real st log (a,b) >= log (c,d) & a < b holds
c > d