let A, B be Ordinal; :: thesis: for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))
let R, S be Relation; :: thesis: ( R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) implies R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) )
assume that
A1: ( R is almost-No-order & S is almost-No-order ) and
A2: R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) and
A3: ( R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis: R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))
defpred S₁[ Ordinal] means ( $1 c= B implies R /\ (ClosedProd (R,A,$1)) = S /\ (ClosedProd (S,A,$1)) );
A4: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] by A1, A2, Th20;
A5: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A6: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A7: D c= B ; :: thesis: R /\ (ClosedProd (R,A,D)) = S /\ (ClosedProd (S,A,D))
then ( ClosedProd (R,A,D) c= ClosedProd (R,A,B) & ClosedProd (S,A,D) c= ClosedProd (S,A,B) ) by Th17;
then A8: ( R preserves_No_Comparison_on ClosedProd (R,A,D) & S preserves_No_Comparison_on ClosedProd (S,A,D) ) by A3;
A9: R /\ (OpenProd (R,A,D)) c= S /\ (OpenProd (S,A,D))

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R /\ (OpenProd (R,A,D)) or [x,y] in S /\ (OpenProd (S,A,D)) )
assume A10: [x,y] in R /\ (OpenProd (R,A,D)) ; :: thesis: [x,y] in S /\ (OpenProd (S,A,D))
then A11: ( [x,y] in R & [x,y] in OpenProd (R,A,D) ) by XBOOLE_0:def 4;
A12: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87, A10;
then A13: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A4, Th11;

per cases ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in D ) or ( born (R,x) in D & born (R,y) = A ) ) by A11, A12, Def9;

suppose ( born (R,x) in A & born (R,y) in A ) ; :: thesis: [x,y] in S /\ (OpenProd (S,A,D))

then [x,y] in OpenProd (R,A,0) by A12, Def9;
then A14: [x,y] in S /\ (OpenProd (S,A,0)) by A2, A11, XBOOLE_0:def 4;
then A15: ( [x,y] in S & [x,y] in OpenProd (S,A,0) ) by XBOOLE_0:def 4;
A16: ( x in Day (S,A) & y in Day (S,A) ) by A14, ZFMISC_1:87;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) in {} ) or ( born (S,x) in {} & born (S,y) = A ) ) by A15, Def9;
then [x,y] in OpenProd (S,A,D) by A16, Def9;
hence [x,y] in S /\ (OpenProd (S,A,D)) by A15, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A17: ( born (R,x) = A & born (R,y) in D ) ; :: thesis: [x,y] in S /\ (OpenProd (S,A,D))

then [x,y] in ClosedProd (R,A,(born (R,y))) by A12, Def10;
then A18: [x,y] in R /\ (ClosedProd (R,A,(born (R,y)))) by A11, XBOOLE_0:def 4;
A19: ClosedProd (S,A,(born (R,y))) c= OpenProd (S,A,D) by Th18, A17;
[x,y] in S /\ (ClosedProd (S,A,(born (R,y)))) by A7, A17, A6, A18, ORDINAL1:def 2;
then ( [x,y] in S & [x,y] in ClosedProd (S,A,(born (S,y))) ) by A13, XBOOLE_0:def 4;
hence [x,y] in S /\ (OpenProd (S,A,D)) by A19, A13, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A20: ( born (R,x) in D & born (R,y) = A ) ; :: thesis: [x,y] in S /\ (OpenProd (S,A,D))

then [x,y] in ClosedProd (R,A,(born (R,x))) by A12, Def10;
then A21: [x,y] in R /\ (ClosedProd (R,A,(born (R,x)))) by A11, XBOOLE_0:def 4;
A22: ClosedProd (S,A,(born (R,x))) c= OpenProd (S,A,D) by Th18, A20;
[x,y] in S /\ (ClosedProd (S,A,(born (R,x)))) by A7, A20, A6, A21, ORDINAL1:def 2;
then ( [x,y] in S & [x,y] in ClosedProd (S,A,(born (S,x))) ) by A13, XBOOLE_0:def 4;
hence [x,y] in S /\ (OpenProd (S,A,D)) by XBOOLE_0:def 4, A22, A13; :: thesis: verum

end;

end;

end;

S /\ (OpenProd (S,A,D)) c= R /\ (OpenProd (R,A,D))

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in S /\ (OpenProd (S,A,D)) or [x,y] in R /\ (OpenProd (R,A,D)) )
assume A23: [x,y] in S /\ (OpenProd (S,A,D)) ; :: thesis: [x,y] in R /\ (OpenProd (R,A,D))
then A24: ( [x,y] in S & [x,y] in OpenProd (S,A,D) ) by XBOOLE_0:def 4;
A25: ( x in Day (S,A) & y in Day (S,A) ) by ZFMISC_1:87, A23;
then A26: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A4, Th11;

per cases ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) in D ) or ( born (S,x) in D & born (S,y) = A ) ) by A24, A25, Def9;

suppose ( born (S,x) in A & born (S,y) in A ) ; :: thesis: [x,y] in R /\ (OpenProd (R,A,D))

then [x,y] in OpenProd (S,A,0) by A25, Def9;
then A27: [x,y] in R /\ (OpenProd (R,A,0)) by A2, A24, XBOOLE_0:def 4;
then A28: ( [x,y] in R & [x,y] in OpenProd (R,A,0) ) by XBOOLE_0:def 4;
A29: ( x in Day (R,A) & y in Day (R,A) ) by A27, ZFMISC_1:87;
then ( born (R,x) in A & born (R,y) in A ) by A28, Def9;
then [x,y] in OpenProd (R,A,D) by A29, Def9;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A28, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A30: ( born (S,x) = A & born (S,y) in D ) ; :: thesis: [x,y] in R /\ (OpenProd (R,A,D))

then [x,y] in ClosedProd (S,A,(born (S,y))) by A25, Def10;
then A31: [x,y] in S /\ (ClosedProd (S,A,(born (S,y)))) by A24, XBOOLE_0:def 4;
A32: ClosedProd (R,A,(born (S,y))) c= OpenProd (R,A,D) by Th18, A30;
[x,y] in R /\ (ClosedProd (R,A,(born (R,y)))) by A26, A6, A30, A31, A7, ORDINAL1:def 2;
then ( [x,y] in R & [x,y] in ClosedProd (R,A,(born (R,y))) ) by XBOOLE_0:def 4;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A32, A26, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A33: ( born (S,x) in D & born (S,y) = A ) ; :: thesis: [x,y] in R /\ (OpenProd (R,A,D))

then [x,y] in ClosedProd (S,A,(born (S,x))) by A25, Def10;
then A34: [x,y] in S /\ (ClosedProd (S,A,(born (S,x)))) by A24, XBOOLE_0:def 4;
A35: ClosedProd (R,A,(born (S,x))) c= OpenProd (R,A,D) by Th18, A33;
[x,y] in R /\ (ClosedProd (R,A,(born (S,x)))) by A7, A33, A6, A34, ORDINAL1:def 2;
then ( [x,y] in R & [x,y] in ClosedProd (R,A,(born (R,x))) ) by A26, XBOOLE_0:def 4;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A35, A26, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence R /\ (ClosedProd (R,A,D)) = S /\ (ClosedProd (S,A,D)) by A1, A8, Th21, A9, XBOOLE_0:def 10; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A5);
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) ; :: thesis: verum