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, ACL;
hence c < d by XREAL_1:118; :: thesis: verum