for G being non empty multLoopStr
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) & 1. G in D holds
ex H being non empty strict MonoidalSubStr of G st the carrier of H = D