:: deftheorem Def18 defines born SURREAL0:def 18 :
for x being Surreal
for b₂ being Ordinal holds
( b₂ = born x iff ( x in Day b₂ & ( for O being Ordinal st x in Day O holds
b₂ c= O ) ) );