( ( for Q being multLoop st Q is satisfying_TT & Q is satisfying_TL & Q is satisfying_TR & Q is satisfying_LR & Q is satisfying_LL & Q is satisfying_RR holds
( Q is satisfying_aa1 & Q is satisfying_aa2 & Q is satisfying_aa3 & Q is satisfying_Ka & Q is satisfying_aK1 & Q is satisfying_aK2 & Q is satisfying_aK3 ) ) implies for Q being AIM multLoop holds
( Q _/_ (lp (Nucl Q)) is commutative multGroup & Q _/_ (lp (Cent Q)) is multGroup ) )