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