let a, b, c be Real; ( a > 1 & b >= a & c >= 1 implies log (a,c) >= log (b,c) )
assume that
A1:
a > 1
and
A2:
b >= a
and
A3:
c >= 1
; log (a,c) >= log (b,c)
b > 1
by A1, A2, XXREAL_0:2;
then
log (b,c) >= log (b,1)
by A3, PRE_FF:10;
then A4:
log (b,c) >= 0
by A1, A2, POWER:51;
log (a,b) >= log (a,a)
by A1, A2, PRE_FF:10;
then
log (a,b) >= 1
by A1, POWER:52;
then
(log (a,b)) * (log (b,c)) >= 1 * (log (b,c))
by A4, XREAL_1:64;
hence
log (a,c) >= log (b,c)
by A1, A2, A3, POWER:56; verum