theorem :: GROUP_9:9

for O being set
for G being GroupWithOperators of O
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g1 being Element of G st g1 in A holds
g1 " in A ) & ( for o being Element of O
for g1 being Element of G st g1 in A holds
(G ^ o) . g1 in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A by Lm14;