let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder holds
s1 = s2
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder holds
s1 = s2
let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder implies s1 = s2 )
assume A1: s1 is_finer_than s2 ; :: thesis: ( not s1 is jordan_holder or not s2 is jordan_holder or s1 = s2 )
assume s1 is jordan_holder ; :: thesis: ( not s2 is jordan_holder or s1 = s2 )
then A2: s1 is strictly_decreasing by Def34;
assume ( s2 is jordan_holder & s1 <> s2 ) ; :: thesis: contradiction
hence contradiction by A1, A2, Def34; :: thesis: verum