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 )
set s29 = the_schreier_series_of (s2,s1);
set s19 = the_schreier_series_of (s1,s2);
take the_schreier_series_of (s1,s2) ; :: thesis: ex s29 being CompositionSeries of G st
( the_schreier_series_of (s1,s2) is_finer_than s1 & s29 is_finer_than s2 & the_schreier_series_of (s1,s2) is_equivalent_with s29 )
take the_schreier_series_of (s2,s1) ; :: thesis: ( the_schreier_series_of (s1,s2) is_finer_than s1 & the_schreier_series_of (s2,s1) is_finer_than s2 & the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) )
thus ( the_schreier_series_of (s1,s2) is_finer_than s1 & the_schreier_series_of (s2,s1) is_finer_than s2 ) by A1, Th116; :: thesis: the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1)
thus the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1) by A1, Th117; :: thesis: verum
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 A2, A3, Th114; :: thesis: s2 is_equivalent_with s2
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 A2, A4, Th114; :: thesis: s1 is_equivalent_with s1
thus s1 is_equivalent_with s1 by Th113; :: thesis: verum
end;
end;
end;
end;