let a, b, c be real number ; :: thesis: ( a > 1 & b > 0 & c >= b implies log a,c >= log a,b )
assume A1: ( a > 1 & b > 0 & c >= b ) ; :: thesis: log a,c >= log a,b
then ( c > b or c = b ) by XXREAL_0:1;
hence log a,c >= log a,b by A1, POWER:65; :: thesis: verum