theorem Th114: :: GROUP_9:114

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds
s2 is_finer_than s1