:: deftheorem Def5 defines born_eq SURREALO:def 5 :
for x being Surreal
for b₂ being Ordinal holds
( b₂ = born_eq x iff ( ex y being Surreal st
( born y = b₂ & y == x ) & ( for y being Surreal st y == x holds
b₂ c= born y ) ) );