theorem Th37: :: AIMLOOP:40

for Q being multLoop
for H being SubLoop of Q
for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds
x * y in the carrier of H