theorem :: AIMLOOP:8

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