consider O being Ordinal such that
A1: x in Day O by Def14;
take b = born ((No_Ord O),x); :: thesis: ( x in Day b & ( for O being Ordinal st x in Day O holds
b c= O ) )
A2: b c= O by A1, Def8;
A3: x in Day ((No_Ord O),b) by Def8, A1;
hence x in Day b by A2, Th36; :: thesis: for O being Ordinal st x in Day O holds
b c= O
let A be Ordinal; :: thesis: ( x in Day A implies b c= A )
assume A4: x in Day A ; :: thesis: b c= A
(No_Ord b) /\ [:(BeforeGames b),(BeforeGames b):] = (No_Ord O) /\ [:(BeforeGames b),(BeforeGames b):] by A2, Th31;
then A5: b = born ((No_Ord b),x) by A3, Th11;
A6: born ((No_Ord A),x) c= A by A4, Def8;
assume A7: not b c= A ; :: thesis: contradiction
then (No_Ord b) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] by Th31;
hence contradiction by A5, A7, A6, Th11, A4; :: thesis: verum