:: deftheorem Def23 defines SubStr MONOID_0:def 23 :
for G, b₂ being multMagma holds
( b₂ is SubStr of G iff the multF of b₂ c= the multF of G );