let A, B, X be Ordinal; :: thesis: ( X c= A & X c= B implies (No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):] )
assume A1: ( X c= A & X c= B ) ; :: thesis: (No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):]
set SA = No_Ord A;
set SB = No_Ord B;
[:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) by Lm3;
then A2: No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),A,A) by Def12;
( A c= X or X in A ) by ORDINAL1:16;
then ( X = A or X in A ) by A1, XBOOLE_0:def 10;
then ClosedProd ((No_Ord A),X,X) c= ClosedProd ((No_Ord A),A,A) by Th17;
then A3: No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),X,X) by A2;
[:(Day ((No_Ord B),B)),(Day ((No_Ord B),B)):] = ClosedProd ((No_Ord B),B,B) by Lm3;
then A4: No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),B,B) by Def12;
( B c= X or X in B ) by ORDINAL1:16;
then ( X = B or X in B ) by A1, XBOOLE_0:def 10;
then ClosedProd ((No_Ord B),X,X) c= ClosedProd ((No_Ord B),B,B) by Th17;
then No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),X,X) by A4;
then A5: (No_Ord A) /\ (ClosedProd ((No_Ord A),X,X)) = (No_Ord B) /\ (ClosedProd ((No_Ord B),X,X)) by Th23, A3;
( ClosedProd ((No_Ord A),X,X) = OpenProd ((No_Ord A),X,(succ X)) & ClosedProd ((No_Ord B),X,X) = OpenProd ((No_Ord B),X,(succ X)) ) by ORDINAL1:6, Th29;
hence (No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):] by A5, Th20; :: thesis: verum