theorem Th15: :: GROUP_9:15

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