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