theorem :: GROUP_9:73

for O being set
for G being GroupWithOperators of O
for B, C being Subset of G st B = the carrier of (gr C) holds
the_stable_subgroup_of C = the_stable_subgroup_of B by Lm31;