:: deftheorem Def25 defines Comm AIMLOOP:def 25 :
for Q being multLoop
for b₂ being Subset of Q holds
( b₂ = Comm Q iff for x being Element of Q holds
( x in b₂ iff for y being Element of Q holds x * y = y * x ) );