theorem Th77: :: GROUP_9:77

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial