:: deftheorem defines non-increasing BAGORDER:def 3 :
for R being non empty RelStr
for s being sequence of R holds
( s is non-increasing iff for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R );