for M being non empty multLoopStr
for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 c= the carrier of H2 holds
H1 is MonoidalSubStr of H2