theorem Th12: :: AIMLOOP:12
for Q being multLoop
for x being Element of Q holds
( x in Nucl Q iff ( x in Nucl_l Q & x in Nucl_m Q & x in Nucl_r Q ) )