:: deftheorem Def3 defines / AIMLOOP:def 3 :
for Q being non empty right_mult-cancelable invertible multLoopStr
for x, y, b₄ being Element of Q holds
( b₄ = x / y iff b₄ * y = x );