:: deftheorem defines ascending DICKSON:def 1 :
for R being RelStr
for f being sequence of R holds
( f is ascending iff for n being Element of NAT holds
( f . (n + 1) <> f . n & [(f . n),(f . (n + 1))] in the InternalRel of R ) );