:: deftheorem Def7 defines decreasing_infinitely SURREAL1:def 7 :
for S being Surreal-Sequence holds
( S is decreasing_infinitely iff for A, B being Ordinal st A in B & B in dom S holds
S .. B infinitely< S .. A );