theorem Th3: :: DICKSON:4

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