theorem Th97: :: SURREALC:97
for r being Sequence of REAL
for y being Surreal-Sequence
for s being uSurreal-Sequence
for alpha being Ordinal st s,y,r simplest_up_to alpha & s | alpha is one-to-one holds
(born s) | alpha is increasing