theorem :: MONOID_1:24

for X being set
for G being non empty multMagma
for H being non empty SubStr of G holds .: (H,X) is SubStr of .: (G,X)