let a, b, c be Real; :: thesis: ( a > 0 & a < 1 & b > 0 & c > b implies log (a,c) < log (a,b) )
assume that
A1: ( a > 0 & a < 1 ) and
A2: b > 0 and
A3: c > b and
A4: log (a,c) >= log (a,b) ; :: thesis: contradiction
A5: a to_power (log (a,b)) = b by A1, A2, Def3;
A6: a to_power (log (a,c)) = c by A1, A2, A3, Def3;

now :: thesis: contradiction

per cases ( log (a,c) > log (a,b) or log (a,c) = log (a,b) ) by A4, XXREAL_0:1;

suppose log (a,c) > log (a,b) ; :: thesis: contradiction

hence contradiction by A1, A3, A5, A6, Th40; :: thesis: verum

end;

suppose log (a,c) = log (a,b) ; :: thesis: contradiction

hence contradiction by A1, A2, A3, A6, Def3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum