theorem Th118: :: GROUP_9:118

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )