let O be set ; :: thesis: 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 )

let G be GroupWithOperators of O; :: thesis: 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 )

let s1, s2 be CompositionSeries of G; :: thesis: ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

per cases ( ( len s1 > 1 & len s2 > 1 ) or len s1 <= 1 or len s2 <= 1 ) ;
suppose A1: ( len s1 > 1 & len s2 > 1 ) ; :: thesis: ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

end;
suppose A2: ( len s1 <= 1 or len s2 <= 1 ) ; :: thesis: ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

per cases ( len s1 <= len s2 or len s1 > len s2 ) ;
suppose A3: len s1 <= len s2 ; :: thesis: ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

set s29 = s2;
set s19 = s2;
take s2 ; :: thesis: ex s29 being CompositionSeries of G st
( s2 is_finer_than s1 & s29 is_finer_than s2 & s2 is_equivalent_with s29 )

take s2 ; :: thesis: ( s2 is_finer_than s1 & s2 is_finer_than s2 & s2 is_equivalent_with s2 )
thus ( s2 is_finer_than s1 & s2 is_finer_than s2 ) by ; :: thesis:
thus s2 is_equivalent_with s2 by Th113; :: thesis: verum
end;
suppose A4: len s1 > len s2 ; :: thesis: ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

set s29 = s1;
set s19 = s1;
take s1 ; :: thesis: ex s29 being CompositionSeries of G st
( s1 is_finer_than s1 & s29 is_finer_than s2 & s1 is_equivalent_with s29 )

take s1 ; :: thesis: ( s1 is_finer_than s1 & s1 is_finer_than s2 & s1 is_equivalent_with s1 )
thus ( s1 is_finer_than s1 & s1 is_finer_than s2 ) by ; :: thesis:
thus s1 is_equivalent_with s1 by Th113; :: thesis: verum
end;
end;
end;
end;