theorem Th20c: :: AIMLOOP:22

for Q being multLoop holds 1. Q in Nucl_r Q