:: deftheorem defines @ AIMLOOP:def 33 :
for Q being non empty multLoopStr
for H being SubLoopStr of Q
for A being Subset of H holds @ A = A;