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

now

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

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

hence contradiction by A1, A3, A4, Th45; :: thesis: verum

end;

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

hence contradiction by A1, A4, Def3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum