:: deftheorem Def8 defines " LOPBAN_3:def 8 :
for X being non empty well-unital associative multLoopStr
for x being Element of X st x is invertible holds
for b₃ being Element of the carrier of X holds
( b₃ = x " iff ( x * b₃ = 1. X & b₃ * x = 1. X ) );