let a, b, c be Real; :: thesis: ( 1 < a & 0 < b & b <= c implies log (a,b) <= log (a,c) )
assume AS: ( 1 < a & 0 < b & b <= c ) ; :: thesis: log (a,b) <= log (a,c)

now :: thesis: ( ( b < c & log (a,b) < log (a,c) ) or ( b = c & log (a,b) = log (a,c) ) )

per cases ( b < c or b = c ) by AS, XXREAL_0:1;

case b < c ; :: thesis: log (a,b) < log (a,c)

hence log (a,b) < log (a,c) by POWER:57, AS; :: thesis: verum

end;

case b = c ; :: thesis: log (a,b) = log (a,c)

hence log (a,b) = log (a,c) ; :: thesis: verum

end;

end;

end;

hence log (a,b) <= log (a,c) ; :: thesis: verum