theorem Th99: :: GROUP_9:99

for O being set
for G being GroupWithOperators of O
for s1, s19, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds
s19 is_finer_than s2