theorem Th31: :: MONOID_0:31

for M being non empty well-unital multLoopStr
for N being non empty MonoidalSubStr of M holds N is well-unital