let a, b, c be Real; :: thesis: ( a > 1 & b > 0 & c >= b implies log (a,c) >= log (a,b) )
assume that
A1: ( a > 1 & b > 0 ) and
A2: c >= b ; :: thesis: log (a,c) >= log (a,b)
( c > b or c = b ) by A2, XXREAL_0:1;
hence log (a,c) >= log (a,b) by A1, POWER:57; :: thesis: verum