theorem Th38: :: AIMLOOP:41

for Q being multLoop
for H being SubLoop of Q
for x, y being Element of Q
for x1, y1 being Element of H st x = x1 & y = y1 holds
x \ y = x1 \ y1