theorem :: GROUP_9:5

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G in H1 by Lm17;