let A, B be Ordinal; :: thesis: ( A c= B implies ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A) )
assume A c= B ; :: thesis: ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A)
then (No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord B) /\ [:(BeforeGames A),(BeforeGames A):] by Th31;
hence ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A) by Th15; :: thesis: verum