theorem Th96: :: GROUP_9:96

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s2 = len s1 & s2 is_finer_than s1 holds
s1 = s2