for R being non empty transitive RelStr
for f being sequence of R st f is weakly-ascending holds
for i, j being Nat st i < j holds
f . i <= f . j