for R being non empty RelStr
for s being sequence of R st R is Dickson holds
ex t being sequence of R st
( t is subsequence of s & t is weakly-ascending )