:: deftheorem Def22 defines name-r SURREALC:def 22 :
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₂,y) == x ) );