theorem :: AIMLOOP:7

for Q being multLoop
for x, y being Element of Q st x \ y = 1. Q holds
x = y