:: deftheorem defines non-descending SURREAL1:def 2 :
for R being non empty RelStr
for s being sequence of R holds
( s is non-descending iff for n being Nat holds [(s . n),(s . (n + 1))] in the InternalRel of R );