:: deftheorem Def8 defines born SURREAL0:def 8 :
for R being Relation
for o being object st ex O being Ordinal st o in Day (R,O) holds
for b₃ being Ordinal holds
( b₃ = born (R,o) iff ( o in Day (R,b₃) & ( for O being Ordinal st o in Day (R,O) holds
b₃ c= O ) ) );