theorem CPOWER57: :: ASYMPT_2:7

for a, b, c being Real st 1 < a & 0 < b & b <= c holds
log (a,b) <= log (a,c)