theorem :: GROUP_9:8

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
g1 " in H1 by Lm19;