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 ) 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;

A7: now

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

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

thus contradiction by A1, A3, A5, A6, A8, Th45; :: thesis: verum

end;

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

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

end;

end;

end;

thus contradiction by A7; :: thesis: verum