let A, B be Ordinal; :: thesis: ( B c= A implies for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B)) )
assume A1: B c= A ; :: thesis: for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) c= 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,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) implies R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B)) )
assume that
A2: ( R is almost-No-order & S is almost-No-order ) and
A3: R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) and
A4: ( R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis: R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B))
A5: S /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by Th20, A2, A3;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R /\ (ClosedProd (R,A,B)) or [x,y] in S /\ (ClosedProd (S,A,B)) )
A6: ( OpenProd (R,A,B) c= ClosedProd (R,A,B) & OpenProd (S,A,B) c= ClosedProd (S,A,B) ) by Th16;
assume A7: [x,y] in R /\ (ClosedProd (R,A,B)) ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))
then A8: ( [x,y] in R & [x,y] in ClosedProd (R,A,B) ) by XBOOLE_0:def 4;
reconsider x = x, y = y as Element of Day (R,A) by ZFMISC_1:87, A7;
x <= R,y by A7, XBOOLE_0:def 4;
then A9: ( L_ x << R,{y} & {x} << R, R_ y ) by A8, A4;
A10: [x,y] in ClosedProd (R,A,B) by A7, XBOOLE_0:def 4;

per cases then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,y) = A & born (R,x) c= B ) ) by Def10;

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

then [x,y] in OpenProd (R,A,B) by Def9;
then [x,y] in S /\ (OpenProd (S,A,B)) by A3, A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

suppose A11: ( born (R,x) = A & born (R,y) c= B ) ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))

per cases ( born (R,y) = B or born (R,y) <> B ) ;

suppose A12: born (R,y) = B ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))

A13: Day (R,A) = Day (S,A) by A5, Th10;
A14: ClosedProd (R,A,B) = ClosedProd (S,A,B) by A5, Th15;
A15: L_ x << S,{y}

proof

given l, r being object such that A16: ( l in L_ x & r in {y} & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A17: r = y by A16, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A16, XBOOLE_0:def 3;
then consider O being Ordinal such that
A18: ( O in A & l in Day (R,O) ) by Th7;
A19: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) ) by Th9, A5, Th10, A18, ORDINAL1:def 2;
born (S,l) c= O by A18, A19, Def8;
then A20: born (S,l) in A by ORDINAL1:12, A18;
A21: born (S,y) = B by A12, Th11, A5;
[y,l] in OpenProd (S,A,B)

proof

per cases ( A = B or A <> B ) ;

suppose A = B ; :: thesis: [y,l] in OpenProd (S,A,B)

hence [y,l] in OpenProd (S,A,B) by A20, Def9, A19, A18, A13, A21; :: thesis: verum

end;

suppose A <> B ; :: thesis: [y,l] in OpenProd (S,A,B)

then B in A by ORDINAL1:11, A1, XBOOLE_0:def 8;
hence [y,l] in OpenProd (S,A,B) by A20, Def9, A19, A18, A13, A21; :: thesis: verum

end;

end;

end;

then [y,l] in R /\ (OpenProd (R,A,B)) by A3, A16, A17, XBOOLE_0:def 4;
then l >= R,r by A17, XBOOLE_0:def 4;
hence contradiction by A9, A16; :: thesis: verum

end;

A22: {x} << S, R_ y

proof

given l, r being object such that A23: ( l in {x} & r in R_ y & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A24: l = x by A23, TARSKI:def 1;
A25: y in Day (R,B) by A12, Def8;
r in (L_ y) \/ (R_ y) by A23, XBOOLE_0:def 3;
then consider O being Ordinal such that
A26: ( O in B & r in Day (R,O) ) by A25, Th7;
A27: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) & Day (R,A) = Day (S,A) ) by Th9, A5, Th10, A1, A26, ORDINAL1:def 2;
born (S,r) c= O by A26, A27, Def8;
then A28: born (S,r) in B by A26, ORDINAL1:12;
born (S,x) = A by A11, Th11, A5;
then [r,x] in OpenProd (S,A,B) by A28, Def9, A27, A26;
then [r,x] in S /\ (OpenProd (S,A,B)) by A23, A24, XBOOLE_0:def 4;
then l >= R,r by A24, A3, XBOOLE_0:def 4;
hence contradiction by A9, A23; :: thesis: verum

end;

x <= S,y by A15, A22, A4, A14, A10;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A14, A10, XBOOLE_0:def 4; :: thesis: verum

end;

suppose born (R,y) <> B ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))

then born (R,y) in B by A11, XBOOLE_0:def 8, ORDINAL1:11;
then [x,y] in OpenProd (R,A,B) by A11, Def9;
then [x,y] in R /\ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by A3, XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

suppose A29: ( born (R,y) = A & born (R,x) c= B ) ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))

per cases ( born (R,x) = B or born (R,x) <> B ) ;

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

A31: Day (R,A) = Day (S,A) by A5, Th10;
A32: ClosedProd (R,A,B) = ClosedProd (S,A,B) by A5, Th15;
A33: L_ x << S,{y}

proof

given l, r being object such that A34: ( l in L_ x & r in {y} & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A35: r = y by A34, TARSKI:def 1;
A36: x in Day (R,B) by A30, Def8;
l in (L_ x) \/ (R_ x) by A34, XBOOLE_0:def 3;
then consider O being Ordinal such that
A37: ( O in B & l in Day (R,O) ) by A36, Th7;
A38: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) & Day (R,A) = Day (S,A) ) by Th9, A5, Th10, A1, A37, ORDINAL1:def 2;
born (S,l) c= O by A37, A38, Def8;
then A39: born (S,l) in B by A37, ORDINAL1:12;
born (S,y) = A by A29, Th11, A5;
then [y,l] in OpenProd (S,A,B) by A39, Def9, A37, A38;
then [y,l] in R /\ (OpenProd (R,A,B)) by A3, A34, A35, XBOOLE_0:def 4;
then l >= R,r by A35, XBOOLE_0:def 4;
hence contradiction by A9, A34; :: thesis: verum

end;

A40: {x} << S, R_ y

proof

given l, r being object such that A41: ( l in {x} & r in R_ y & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A42: l = x by A41, TARSKI:def 1;
r in (L_ y) \/ (R_ y) by A41, XBOOLE_0:def 3;
then consider O being Ordinal such that
A43: ( O in A & r in Day (R,O) ) by Th7;
A44: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) ) by Th9, A5, Th10, A43, ORDINAL1:def 2;
born (S,r) c= O by A43, A44, Def8;
then A45: born (S,r) in A by ORDINAL1:12, A43;
A46: born (S,x) = B by A30, Th11, A5;
[r,x] in OpenProd (S,A,B)

proof

per cases ( A = B or A <> B ) ;

suppose A = B ; :: thesis: [r,x] in OpenProd (S,A,B)

hence [r,x] in OpenProd (S,A,B) by A45, A31, Def9, A44, A43, A46; :: thesis: verum

end;

suppose A <> B ; :: thesis: [r,x] in OpenProd (S,A,B)

then B in A by ORDINAL1:11, A1, XBOOLE_0:def 8;
hence [r,x] in OpenProd (S,A,B) by A45, A31, Def9, A44, A43, A46; :: thesis: verum

end;

end;

end;

then [r,x] in S /\ (OpenProd (S,A,B)) by A41, A42, XBOOLE_0:def 4;
then l >= R,r by A3, A42, XBOOLE_0:def 4;
hence contradiction by A9, A41; :: thesis: verum

end;

x <= S,y by A32, A10, A33, A40, A4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A32, A10, XBOOLE_0:def 4; :: thesis: verum

end;

suppose born (R,x) <> B ; :: thesis: [x,y] in S /\ (ClosedProd (S,A,B))

then born (R,x) in B by ORDINAL1:11, A29, XBOOLE_0:def 8;
then [x,y] in OpenProd (R,A,B) by A29, Def9;
then [x,y] in R /\ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by A3, XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

end;