theorem Th22: :: AIMLOOP:25

for Q being multLoop
for x, y being Element of Q st x in Nucl Q & y in Nucl Q holds
x \ y in Nucl Q