:: deftheorem DM defines DershowitzMannaOrder BAGORD_2:def 4 :
for R being non empty RelStr
for b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = DershowitzMannaOrder R iff for m, n being Element of b₂ holds
( m <= n iff ex x, y being Element of b₂ st
( 1. b₂ <> x & x divides n & m = (n -' x) + y & ( for b being Element of R st y . b > 0 holds
ex a being Element of R st
( x . a > 0 & b <= a ) ) ) ) );