let a be positive heavy Real; for c being positive light Real
for b, d being positive Real st log (a,b) >= log (c,d) & a > b holds
c < d
let c be positive light Real; for b, d being positive Real st log (a,b) >= log (c,d) & a > b holds
c < d
let b, d be positive Real; ( log (a,b) >= log (c,d) & a > b implies c < d )
assume A2:
( log (a,b) >= log (c,d) & a > b )
; c < d
then
log (a,b) < 1
by AG1;
then
log (c,d) < 1
by A2, XXREAL_0:2;
hence
c < d
by AM1; verum