let a, b, c be real number ; :: 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:65; :: thesis: verum