:: deftheorem defines co-ordered BAGORD_2:def 9 :
for R being RelStr
for M being RelExtension of finite-MultiSet_over the carrier of R
for b being Element of M
for p being partition of b holds
( p is co-ordered iff for i being Nat st i in dom p & i + 1 in dom p holds
for b1, b2 being Element of M st b1 = p . i & b2 = p . (i + 1) holds
b2 <= b1 );