theorem :: GROUP_9:7

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G st g1 in H1 & g2 in H1 holds
g1 * g2 in H1 by Lm18;