for R being non empty transitive asymmetric RelStr
for b being bag of the carrier of R
for x being Element of R
for q being partition of b st q is ordered & (q /. 1) . x = 0 & b . x > 0 holds
ex y being Element of R st
( (q /. 1) . y > 0 & x <= y )