for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st not s1 is empty & s2 is_finer_than s1 holds
not s2 is empty ;