theorem Th113: :: GROUP_9:113

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G holds s1 is_equivalent_with s1