theorem Th8: :: BAGORDER:9

for R being non empty transitive RelStr
for f being sequence of R st f is non-increasing holds
for j, i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R