theorem Th98: :: SURREALC:98

for x being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for s being uSurreal-Sequence
for A being Ordinal st A c= dom r & x in_meets_terms s,y,r,A & s,y,r simplest_up_to succ A holds
rng (born (s | (succ A))) c= succ (born_eq x)