:: deftheorem Def3 defines log POWER:def 3 :
for a, b being Real st a > 0 & a <> 1 & b > 0 holds
for b₃ being Real holds
( b₃ = log (a,b) iff a to_power b₃ = b );