:: deftheorem defines \ AIMLOOP:def 45 :
for Q being multLoopStr
for H1, H2, b₄ being Subset of Q holds
( b₄ = H1 \ H2 iff for x being Element of Q holds
( x in b₄ iff ex y, z being Element of Q st
( y in H1 & z in H2 & x = y \ z ) ) );