:: deftheorem PPM defines PrecPrecM BAGORD_2:def 15 :
for R being non empty transitive asymmetric RelStr
for b₂ being strict RelExtension of finite-MultiSet_over the carrier of R holds
( b₂ = PrecPrecM R iff for m, n being Element of b₂ holds
( m <= n iff [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) ) );