theorem Th110: :: GROUP_9:110

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G st len s1 > 1 holds
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )