let a, c be positive light Real; :: thesis: for b, d being positive Real st log (a,b) <= log (c,d) & a > b holds
c > d
let b, d be positive Real; :: thesis: ( log (a,b) <= log (c,d) & a > b implies c > d )
assume A3: ( log (a,b) <= log (c,d) & a > b ) ; :: thesis: c > d
A4: ( log (a,b) = log ((1 / a),(1 / b)) & log (c,d) = log ((1 / c),(1 / d)) ) by ABO;
1 / a < 1 / b by A3, XREAL_1:76;
then 1 / c < 1 / d by A3, A4, ACG;
hence c > d by XREAL_1:118; :: thesis: verum