let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: ( R is almost-No-order & S is almost-No-order & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis:
defpred S₁[ Ordinal] means ( $1 in A implies R /\ (ClosedProd (R,$1,$1)) = S /\ (ClosedProd (S,$1,$1)) );
A2: 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:
assume A3: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
assume A4: D in A ; :: thesis:
( ClosedProd (R,D,D) c= ClosedProd (R,A,B) & ClosedProd (S,D,D) c= ClosedProd (S,A,B) ) by A4, Th17;
then A5: ( R preserves_No_Comparison_on ClosedProd (R,D,D) & S preserves_No_Comparison_on ClosedProd (S,D,D) ) by A1;
A6: R /\ (OpenProd (R,D,0)) c= S /\ (OpenProd (S,D,0))

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A7: [x,y] in R /\ (OpenProd (R,D,0)) ; :: thesis:
A8: ( [x,y] in R & [x,y] in OpenProd (R,D,0) ) by A7, XBOOLE_0:def 4;
A9: ( x in Day (R,D) & y in Day (R,D) ) by A7, ZFMISC_1:87;
then A10: ( born (R,x) in D & born (R,y) in D ) by A8, Def9;
A11: ( x in Day (R,(born (R,x))) & y in Day (R,(born (R,y))) ) by A9, Def8;
A12: ( born (R,x) in A & born (R,y) in A ) by A10, A4, ORDINAL1:10;

per cases by ORDINAL1:16;

suppose A13: born (R,x) c= born (R,y) ; :: thesis:

set b = born (R,y);
Day (R,(born (R,x))) c= Day (R,(born (R,y))) by A13, Th9;
then [x,y] in ClosedProd (R,(born (R,y)),(born (R,y))) by A11, Def10, A13;
then [x,y] in R /\ (ClosedProd (R,(born (R,y)),(born (R,y)))) by A8, XBOOLE_0:def 4;
then A14: [x,y] in S /\ (ClosedProd (S,(born (R,y)),(born (R,y)))) by A10, A12, A3;
then A15: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,y)),(born (R,y))) ) by XBOOLE_0:def 4;
A16: ( x in Day (S,(born (R,y))) & y in Day (S,(born (R,y))) ) by A14, ZFMISC_1:87;
A17: Day (S,(born (R,y))) c= Day (S,D) by A10, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,y) & born (S,y) in born (R,y) ) or ( born (S,x) = born (R,y) & born (S,y) c= born (R,y) ) or ( born (S,x) c= born (R,y) & born (S,y) = born (R,y) ) ) by A15, A16, Def10;
then ( ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) ) by A10, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,D,0) by A17, A16, Def9;
hence [x,y] in S /\ (OpenProd (S,D,0)) by A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A18: born (R,y) in born (R,x) ; :: thesis:

then A19: born (R,y) c= born (R,x) by ORDINAL1:def 2;
set b = born (R,x);
Day (R,(born (R,y))) c= Day (R,(born (R,x))) by A18, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (R,(born (R,x)),(born (R,x))) by A11, Def10, A19;
then [x,y] in R /\ (ClosedProd (R,(born (R,x)),(born (R,x)))) by A8, XBOOLE_0:def 4;
then A20: [x,y] in S /\ (ClosedProd (S,(born (R,x)),(born (R,x)))) by A10, A12, A3;
then A21: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,x)),(born (R,x))) ) by XBOOLE_0:def 4;
A22: ( x in Day (S,(born (R,x))) & y in Day (S,(born (R,x))) ) by ZFMISC_1:87, A20;
A23: Day (S,(born (R,x))) c= Day (S,D) by A10, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,x) & born (S,y) in born (R,x) ) or ( born (S,x) = born (R,x) & born (S,y) c= born (R,x) ) or ( born (S,x) c= born (R,x) & born (S,y) = born (R,x) ) ) by A21, A22, Def10;
then ( ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) ) by A10, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,D,0) by A23, A22, Def9;
hence [x,y] in S /\ (OpenProd (S,D,0)) by A21, XBOOLE_0:def 4; :: thesis:

end;

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

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A24: [x,y] in S /\ (OpenProd (S,D,0)) ; :: thesis:
A25: ( [x,y] in S & [x,y] in OpenProd (S,D,0) ) by A24, XBOOLE_0:def 4;
A26: ( x in Day (S,D) & y in Day (S,D) ) by A24, ZFMISC_1:87;
then A27: ( born (S,x) in D & born (S,y) in D ) by A25, Def9;
A28: ( x in Day (S,(born (S,x))) & y in Day (S,(born (S,y))) ) by A26, Def8;
A29: ( born (S,x) in A & born (S,y) in A ) by A27, A4, ORDINAL1:10;

per cases by ORDINAL1:16;

suppose A30: born (S,x) c= born (S,y) ; :: thesis:

set b = born (S,y);
Day (S,(born (S,x))) c= Day (S,(born (S,y))) by A30, Th9;
then [x,y] in ClosedProd (S,(born (S,y)),(born (S,y))) by A28, Def10, A30;
then [x,y] in S /\ (ClosedProd (S,(born (S,y)),(born (S,y)))) by A25, XBOOLE_0:def 4;
then A31: [x,y] in R /\ (ClosedProd (R,(born (S,y)),(born (S,y)))) by A27, A29, A3;
then A32: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,y)),(born (S,y))) ) by XBOOLE_0:def 4;
A33: ( x in Day (R,(born (S,y))) & y in Day (R,(born (S,y))) ) by A31, ZFMISC_1:87;
A34: Day (R,(born (S,y))) c= Day (R,D) by A27, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,y) & born (R,y) in born (S,y) ) or ( born (R,x) = born (S,y) & born (R,y) c= born (S,y) ) or ( born (R,x) c= born (S,y) & born (R,y) = born (S,y) ) ) by A32, A33, Def10;
then ( ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) ) by A27, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,D,0) by A34, A33, Def9;
hence [x,y] in R /\ (OpenProd (R,D,0)) by A32, XBOOLE_0:def 4; :: thesis:

end;

suppose A35: born (S,y) in born (S,x) ; :: thesis:

then A36: born (S,y) c= born (S,x) by ORDINAL1:def 2;
set b = born (S,x);
Day (S,(born (S,y))) c= Day (S,(born (S,x))) by A35, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (S,(born (S,x)),(born (S,x))) by A28, Def10, A36;
then [x,y] in S /\ (ClosedProd (S,(born (S,x)),(born (S,x)))) by A25, XBOOLE_0:def 4;
then A37: [x,y] in R /\ (ClosedProd (R,(born (S,x)),(born (S,x)))) by A27, A29, A3;
then A38: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,x)),(born (S,x))) ) by XBOOLE_0:def 4;
A39: ( x in Day (R,(born (S,x))) & y in Day (R,(born (S,x))) ) by ZFMISC_1:87, A37;
A40: Day (R,(born (S,x))) c= Day (R,D) by A27, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,x) & born (R,y) in born (S,x) ) or ( born (R,x) = born (S,x) & born (R,y) c= born (S,x) ) or ( born (R,x) c= born (S,x) & born (R,y) = born (S,x) ) ) by A38, A39, Def10;
then ( ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) ) by A27, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,D,0) by A40, A39, Def9;
hence [x,y] in R /\ (OpenProd (R,D,0)) by A38, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ (ClosedProd (R,D,D)) = S /\ (ClosedProd (S,D,D)) by A1, A5, Th22, A6, XBOOLE_0:def 10; :: thesis:

end;

A41: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A2);
A42: R /\ (OpenProd (R,A,0)) c= S /\ (OpenProd (S,A,0))

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A43: [x,y] in R /\ (OpenProd (R,A,0)) ; :: thesis:
A44: ( [x,y] in R & [x,y] in OpenProd (R,A,0) ) by A43, XBOOLE_0:def 4;
A45: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87, A43;
then A46: ( born (R,x) in A & born (R,y) in A ) by A44, Def9;
A47: ( x in Day (R,(born (R,x))) & y in Day (R,(born (R,y))) ) by A45, Def8;

per cases by ORDINAL1:16;

suppose A48: born (R,x) c= born (R,y) ; :: thesis:

set b = born (R,y);
Day (R,(born (R,x))) c= Day (R,(born (R,y))) by A48, Th9;
then [x,y] in ClosedProd (R,(born (R,y)),(born (R,y))) by A47, Def10, A48;
then [x,y] in R /\ (ClosedProd (R,(born (R,y)),(born (R,y)))) by A44, XBOOLE_0:def 4;
then A49: [x,y] in S /\ (ClosedProd (S,(born (R,y)),(born (R,y)))) by A41, A46;
then A50: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,y)),(born (R,y))) ) by XBOOLE_0:def 4;
A51: ( x in Day (S,(born (R,y))) & y in Day (S,(born (R,y))) ) by A49, ZFMISC_1:87;
A52: Day (S,(born (R,y))) c= Day (S,A) by A46, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,y) & born (S,y) in born (R,y) ) or ( born (S,x) = born (R,y) & born (S,y) c= born (R,y) ) or ( born (S,x) c= born (R,y) & born (S,y) = born (R,y) ) ) by A50, A51, Def10;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) ) by A46, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,A,0) by A52, A51, Def9;
hence [x,y] in S /\ (OpenProd (S,A,0)) by A50, XBOOLE_0:def 4; :: thesis:

end;

suppose A53: born (R,y) in born (R,x) ; :: thesis:

then A54: born (R,y) c= born (R,x) by ORDINAL1:def 2;
set b = born (R,x);
Day (R,(born (R,y))) c= Day (R,(born (R,x))) by A53, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (R,(born (R,x)),(born (R,x))) by A47, Def10, A54;
then [x,y] in R /\ (ClosedProd (R,(born (R,x)),(born (R,x)))) by A44, XBOOLE_0:def 4;
then A55: [x,y] in S /\ (ClosedProd (S,(born (R,x)),(born (R,x)))) by A41, A46;
then A56: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,x)),(born (R,x))) ) by XBOOLE_0:def 4;
A57: ( x in Day (S,(born (R,x))) & y in Day (S,(born (R,x))) ) by A55, ZFMISC_1:87;
A58: Day (S,(born (R,x))) c= Day (S,A) by A46, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,x) & born (S,y) in born (R,x) ) or ( born (S,x) = born (R,x) & born (S,y) c= born (R,x) ) or ( born (S,x) c= born (R,x) & born (S,y) = born (R,x) ) ) by A56, A57, Def10;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) ) by A46, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,A,0) by A58, A57, Def9;
hence [x,y] in S /\ (OpenProd (S,A,0)) by A56, XBOOLE_0:def 4; :: thesis:

end;

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

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A59: [x,y] in S /\ (OpenProd (S,A,0)) ; :: thesis:
A60: ( [x,y] in S & [x,y] in OpenProd (S,A,0) ) by A59, XBOOLE_0:def 4;
A61: ( x in Day (S,A) & y in Day (S,A) ) by A59, ZFMISC_1:87;
then A62: ( born (S,x) in A & born (S,y) in A ) by A60, Def9;
A63: ( x in Day (S,(born (S,x))) & y in Day (S,(born (S,y))) ) by A61, Def8;

per cases by ORDINAL1:16;

suppose A64: born (S,x) c= born (S,y) ; :: thesis:

set b = born (S,y);
Day (S,(born (S,x))) c= Day (S,(born (S,y))) by A64, Th9;
then [x,y] in ClosedProd (S,(born (S,y)),(born (S,y))) by A63, Def10, A64;
then [x,y] in S /\ (ClosedProd (S,(born (S,y)),(born (S,y)))) by A60, XBOOLE_0:def 4;
then A65: [x,y] in R /\ (ClosedProd (R,(born (S,y)),(born (S,y)))) by A41, A62;
then A66: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,y)),(born (S,y))) ) by XBOOLE_0:def 4;
A67: ( x in Day (R,(born (S,y))) & y in Day (R,(born (S,y))) ) by A65, ZFMISC_1:87;
A68: Day (R,(born (S,y))) c= Day (R,A) by A62, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,y) & born (R,y) in born (S,y) ) or ( born (R,x) = born (S,y) & born (R,y) c= born (S,y) ) or ( born (R,x) c= born (S,y) & born (R,y) = born (S,y) ) ) by A66, A67, Def10;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) ) by A62, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,A,0) by A68, A67, Def9;
hence [x,y] in R /\ (OpenProd (R,A,0)) by A66, XBOOLE_0:def 4; :: thesis:

end;

suppose A69: born (S,y) in born (S,x) ; :: thesis:

then A70: born (S,y) c= born (S,x) by ORDINAL1:def 2;
set b = born (S,x);
Day (S,(born (S,y))) c= Day (S,(born (S,x))) by A69, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (S,(born (S,x)),(born (S,x))) by A63, Def10, A70;
then [x,y] in S /\ (ClosedProd (S,(born (S,x)),(born (S,x)))) by A60, XBOOLE_0:def 4;
then A71: [x,y] in R /\ (ClosedProd (R,(born (S,x)),(born (S,x)))) by A41, A62;
then A72: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,x)),(born (S,x))) ) by XBOOLE_0:def 4;
A73: ( x in Day (R,(born (S,x))) & y in Day (R,(born (S,x))) ) by A71, ZFMISC_1:87;
A74: Day (R,(born (S,x))) c= Day (R,A) by A62, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,x) & born (R,y) in born (S,x) ) or ( born (R,x) = born (S,x) & born (R,y) c= born (S,x) ) or ( born (R,x) c= born (S,x) & born (R,y) = born (S,x) ) ) by A72, A73, Def10;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) ) by A62, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,A,0) by A74, A73, Def9;
hence [x,y] in R /\ (OpenProd (R,A,0)) by A72, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by A1, Th22, A42, XBOOLE_0:def 10; :: thesis: