let a, b, c be Real; :: thesis: ( 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 ; :: thesis: 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:12;
then A4: log b,c >= 0 by A1, A2, POWER:59;
log a,b >= log a,a by A1, A2, PRE_FF:12;
then log a,b >= 1 by A1, POWER:60;
then (log a,b) * (log b,c) >= 1 * (log b,c) by A4, XREAL_1:66;
hence log a,c >= log b,c by A1, A2, A3, POWER:64; :: thesis: verum