:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :
for G being multMagma
for b₂ being multLoopStr holds
( b₂ is MonoidalSubStr of G iff ( the multF of b₂ c= the multF of G & ( for M being multLoopStr st G = M holds
1. b₂ = 1. M ) ) );