let A, B be Ordinal; :: thesis: for o being object st o in Day ((No_Ord A),B) & B c= A holds
o in Day B
let o be object ; :: thesis: ( o in Day ((No_Ord A),B) & B c= A implies o in Day B )
assume A1: ( o in Day ((No_Ord A),B) & B c= A ) ; :: thesis: o in Day B
then (No_Ord A) /\ [:(BeforeGames B),(BeforeGames B):] = (No_Ord B) /\ [:(BeforeGames B),(BeforeGames B):] by Th31;
hence o in Day B by A1, Th10; :: thesis: verum