:: deftheorem Def10 defines " ALGSTR_1:def 10 :
for L being non empty almost_cancelable almost_invertible multLoopStr_0
for x being Element of L st x <> 0. L holds
for b₃ being Element of the carrier of L holds
( b₃ = x " iff b₃ * x = 1. L );