theorem Th39: :: AIMLOOP:42

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