theorem
:: MONOID_1:25
for
X
being
set
for
G
being non
empty
unital
multMagma
for
H
being non
empty
SubStr
of
G
st
the_unity_wrt
the
multF
of
G
in
the
carrier
of
H
holds
.:
(
H
,
X
) is
MonoidalSubStr
of
.:
(
G
,
X
)