theorem Th24: :: MONOID_0:24

for G being non empty multMagma
for H being non empty SubStr of G holds the multF of H = the multF of G || the carrier of H