theorem :: COMPLEX3:109
for a, c being positive light Real
for b, d being positive Real st log (a,b) <= log (c,d) & a > b holds
c > d