let a, b be positive heavy Real; :: thesis: ( log (a,b) > log (b,a) & log (b,a) >= 1 implies a > b )
A1: ( a > 1 & b > 1 ) by TA1;
assume A2: log (a,b) > log (b,a) ; :: thesis: ( not log (b,a) >= 1 or a > b )
assume log (b,a) >= 1 ; :: thesis: a > b
then B2: log (b,a) >= log (b,b) by A1, POWER:52;
B4: a <> b by A2;
a >= b by A1, B2, POWER:57;
hence a > b by B4, XXREAL_0:1; :: thesis: verum