for R being non empty RelStr st R is Dickson holds
for f being sequence of R ex i, j being Nat st
( i < j & f . i <= f . j )