:: deftheorem Def30 defines SubLoopStr AIMLOOP:def 32 :
for Q, b₂ being non empty multLoopStr holds
( b₂ is SubLoopStr of Q iff ( the carrier of b₂ c= the carrier of Q & the multF of b₂ = the multF of Q || the carrier of b₂ & the OneF of b₂ = the OneF of Q ) );