:: deftheorem defines descending WELLFND1:def 6 :
for R being RelStr
for f being sequence of R holds
( f is descending iff for n being Nat holds
( f . (n + 1) <> f . n & [(f . (n + 1)),(f . n)] in the InternalRel of R ) );