theorem Th117: :: GROUP_9:117

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_equivalent_with the_schreier_series_of (s2,s1)