theorem ACG: :: COMPLEX3:105

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