theorem Th92: :: SURREALC:92

for z being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not z == Sum (r,y) holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
omega-y ((Sum (r,y)) - z) < yA