theorem Th20: :: AIMLOOP:23

for Q being multLoop holds 1. Q in Nucl Q