for R being non empty transitive asymmetric RelStr
for a, b being bag of the carrier of R
for y being Element of R
for q being partition of b
for c being bag of the carrier of R
for r being Bags the carrier of b₁ -valued FinSequence st q is ordered & q = <*a,c*> ^ r & c . y > 0 holds
ex x being Element of R st
( a . x > 0 & y <= x )