theorem Th41: :: AIMLOOP:44

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