for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )