theorem Th60: :: AIMLOOP:63

for Q being multLoop
for x, y being Element of Q holds
( y in x * (lp (Nucl Q)) iff ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & y = u * (x * v) ) )