for G being non empty multMagma
for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )