:: deftheorem Def6 defines born_eq_set SURREALO:def 6 :
for x being Surreal
for b₂ being surreal-membered set holds
( b₂ = born_eq_set x iff for y being Surreal holds
( y in b₂ iff ( y == x & y in Day (born_eq x) ) ) );