theorem ABO: :: COMPLEX3:96

for a being positive non weightless Real
for b being positive Real holds
( log (a,b) = - (log ((1 / a),b)) & log ((1 / a),b) = log (a,(1 / b)) & log (a,b) = - (log (a,(1 / b))) & log (a,b) = log ((1 / a),(1 / b)) )