:: deftheorem defines Cent AIMLOOP:def 27 :
for Q being multLoop holds Cent Q = (Comm Q) /\ (Nucl Q);