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
)