theorem :: MONOID_0:81

for G being non empty multMagma
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) holds
ex H being non empty strict SubStr of G st the carrier of H = D by Lm5;