theorem :: GROUP_9:72

for O being set
for G being GroupWithOperators of O
for B being Subset of G st B is empty holds
the_stable_subgroup_of B = (1). G by Lm24;