:: deftheorem Def23 defines Nucl_m AIMLOOP:def 23 :
for Q being multLoop
for b₂ being Subset of Q holds
( b₂ = Nucl_m Q iff for y being Element of Q holds
( y in b₂ iff for x, z being Element of Q holds (x * y) * z = x * (y * z) ) );