:: deftheorem defines Nucl AIMLOOP:def 26 :
for Q being multLoop holds Nucl Q = ((Nucl_l Q) /\ (Nucl_m Q)) /\ (Nucl_r Q);