theorem :: SURREALC:94

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