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