theorem Th101: :: GROUP_9:101

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, j being Nat st i in dom s1 & j in dom s1 & i <= j & H1 = s1 . i & H2 = s1 . j holds
H2 is StableSubgroup of H1