for R being non empty RelStr
for s being sequence of R
for j being Nat st s is descending holds
s ^\ j is descending