:: deftheorem Def28 defines composition_series GROUP_9:def 28 :
for O being set
for G being GroupWithOperators of O
for IT being FinSequence of the_stable_subgroups_of G holds
( IT is composition_series iff ( IT . 1 = (Omega). G & IT . (len IT) = (1). G & ( for i being Nat st i in dom IT & i + 1 in dom IT holds
for H1, H2 being StableSubgroup of G st H1 = IT . i & H2 = IT . (i + 1) holds
H2 is normal StableSubgroup of H1 ) ) );