let A, B be Ordinal; :: thesis: ( A c= B implies Day A c= Day B )
assume A1: A c= B ; :: thesis: Day A c= Day B
set R = No_Ord A;
set S = No_Ord B;
(No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord B) /\ [:(BeforeGames A),(BeforeGames A):] by A1, Th31;
then Day ((No_Ord A),A) = Day ((No_Ord B),A) by Th10;
hence Day A c= Day B by A1, Th9; :: thesis: verum