:: deftheorem PM defines PrecM BAGORD_2:def 13 :
for R being non empty transitive asymmetric RelStr
for b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = PrecM R iff for m, n being Element of b₂ holds
( m <= n iff ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) ) ) );