theorem :: SURREAL0:38

for A being Ordinal
for x being Surreal st x in Day A holds
born x = born ((No_Ord A),x)