:: deftheorem defines increasing SURREAL1:def 3 :
for R being Relation
for s being Sequence of field R holds
( s is increasing iff for A, B being Ordinal st A in B & B in dom s holds
( s . A <> s . B & [(s . A),(s . B)] in R ) );