theorem Th5: :: AIMLOOP:5

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