:: deftheorem Def38 defines Mlt AIMLOOP:def 40 :
for Q being multLoop
for H being Subset of Q
for b₃ being composition-closed inverse-closed Subset of (Funcs (Q,Q)) holds
( b₃ = Mlt H iff ( H left-right-mult-closed b₃ & ( for X being composition-closed inverse-closed Subset of (Funcs (Q,Q)) st H left-right-mult-closed X holds
b₃ c= X ) ) );