theorem :: COMPLEX3:102

for a, b being positive non weightless Real st log (a,b) <= - 1 holds
( 0 > log (b,a) & log (b,a) >= - 1 )