:: deftheorem defines strictly_decreasing GROUP_9:def 30 :
for O being set
for G being GroupWithOperators of O
for IT being CompositionSeries of G holds
( IT is strictly_decreasing iff for i being Nat st i in dom IT & i + 1 in dom IT holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = IT . i & N = IT . (i + 1) holds
not H ./. N is trivial );