theorem :: ASYMPT_1:94
for a, b, c being Real st a > 1 & b >= a & c >= 1 holds
log (a,c) >= log (b,c) by Lm19;