:: deftheorem defines is_finer_than GROUP_9:def 29 :
for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G holds
( s1 is_finer_than s2 iff ex x being set st
( x c= dom s1 & s2 = s1 * (Sgm x) ) );