let a, b be positive non weightless Real; :: thesis: ( log (a,b) <= - 1 implies ( 0 > log (b,a) & log (b,a) >= - 1 ) )
assume A2: log (a,b) <= - 1 ; :: thesis: ( 0 > log (b,a) & log (b,a) >= - 1 )
A4: log (b,a) = 1 / (log (a,b)) by ABA;
(log (a,b)) / (log (a,b)) >= (- 1) / (log (a,b)) by A2, XREAL_1:73;
then 1 >= - (1 / (log (a,b))) by A2, XCMPLX_1:60;
hence ( 0 > log (b,a) & log (b,a) >= - 1 ) by A4, A2, XREAL_1:26; :: thesis: verum