theorem Th109: :: GROUP_9:109

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds
ex 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 ) )