:: deftheorem defines jordan_holder GROUP_9:def 31 :
for O being set
for G being GroupWithOperators of O
for IT being CompositionSeries of G holds
( IT is jordan_holder iff ( IT is strictly_decreasing & ( for s being CompositionSeries of G holds
( not s <> IT or not s is strictly_decreasing or not s is_finer_than IT ) ) ) );