:: deftheorem Def20 defines born SURREALC:def 20 :
for s being Surreal-Sequence
for b₂ being Ordinal-Sequence holds
( b₂ = born s iff ( dom b₂ = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b₂ . alpha = born sa ) ) );