:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :
for M, b₂ being multLoopStr holds
( b₂ is MonoidalSubStr of M iff ( the multF of b₂ c= the multF of M & 1. b₂ = 1. M ) );