theorem Th23: :: AIMLOOP:26

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