:: deftheorem defines weakly-ascending DICKSON:def 2 :
for R being RelStr
for f being sequence of R holds
( f is weakly-ascending iff for n being Nat holds [(f . n),(f . (n + 1))] in the InternalRel of R );