theorem Th112: :: GROUP_9:112

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for s1 being CompositionSeries of G
for i being Nat st 1 <= i & i <= (len s1) - 1 & H1 = s1 . i & H2 = s1 . (i + 1) holds
H2 is normal StableSubgroup of H1