let A be Ordinal; :: thesis: for x being Surreal st x in Day A holds
born x = born ((No_Ord A),x)
let x be Surreal; :: thesis: ( x in Day A implies born x = born ((No_Ord A),x) )
set bx = born x;
set bS = born ((No_Ord A),x);
assume A1: x in Day A ; :: thesis: born x = born ((No_Ord A),x)
then A2: x in Day ((No_Ord A),(born ((No_Ord A),x))) by Def8;
born ((No_Ord A),x) c= A by A1, Def8;
then x in Day (born ((No_Ord A),x)) by Th36, A2;
then A3: born x c= born ((No_Ord A),x) by Def18;
born x c= A by Def18, A1;
then A4: (No_Ord (born x)) /\ [:(BeforeGames (born x)),(BeforeGames (born x)):] = (No_Ord A) /\ [:(BeforeGames (born x)),(BeforeGames (born x)):] by Th31;
A5: x in Day (born x) by Def18;
then born ((No_Ord (born x)),x) = born ((No_Ord A),x) by A4, Th11;
then born ((No_Ord A),x) c= born x by A5, Def8;
hence born x = born ((No_Ord A),x) by A3, XBOOLE_0:def 10; :: thesis: verum