theorem Th116: :: GROUP_9:116

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1