theorem Th103: :: GROUP_9:103

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for i being Nat st i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds
H is trivial ) holds
( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )