:: deftheorem Def26 defines name-r SURREALC:def 26 :
for x being surreal number
for b₂ being non-zero Sequence of REAL holds
( b₂ = name-r x iff ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom b₂ & Sum (b₂,(No_omega^ y)) == x ) );