:: deftheorem Def33 defines lp AIMLOOP:def 35 :
for Q being multLoop
for H being Subset of Q
for b₃ being strict SubLoop of Q holds
( b₃ = lp H iff ( H c= [#] b₃ & ( for H2 being SubLoop of Q st H c= [#] H2 holds
[#] b₃ c= [#] H2 ) ) );