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