:: deftheorem defines ordered BAGORD_2:def 10 :
for R being non empty RelStr
for b being bag of the carrier of R
for p being partition of b holds
( p is ordered iff ( ( for m being bag of the carrier of R st m in rng p holds
for x being Element of R st m . x > 0 holds
m . x = b . x ) & ( for m being bag of the carrier of R st m in rng p holds
for x, y being Element of R st m . x > 0 & m . y > 0 & x <> y holds
x ## y ) & ( for m being bag of the carrier of R st m in rng p holds
m <> EmptyBag the carrier of R ) & ( for i being Nat st i in dom p & i + 1 in dom p holds
for x being Element of R st (p /. (i + 1)) . x > 0 holds
ex y being Element of R st
( (p /. i) . y > 0 & x <= y ) ) ) );