:: deftheorem Def32 defines loopclose1 AIMLOOP:def 34 :
for Q being multLoop
for H1, H2, b₄ being Subset of Q holds
( b₄ = loopclose1 (H1,H2) iff for x being Element of Q holds
( x in b₄ iff ( x in H1 or x = 1. Q or ex y, z being Element of Q st
( y in H2 & z in H2 & ( x = y * z or x = y \ z or x = y / z ) ) ) ) );