theorem :: GROUP_9:12
for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2 by Lm20;