theorem Th16: :: GROUP_9:16

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1