theorem Th90: :: SURREALC:90
for x, z being Surreal
for r being non-zero Sequence of REAL
for y being Sequence
for s being Surreal-Sequence
for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb