let A, B be Ordinal; :: thesis: for R being Relation st R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) holds
ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )
let R be Relation; :: thesis: ( R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) implies ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) ) )
assume A1: ( R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) ) ; :: thesis: ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )
set CC = { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ;
{ [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } is Relation-like

proof

let z be object ; :: according to RELAT_1:def 1 :: thesis: ( not z in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } or ex b₁, b₂ being object st z = [b₁,b₂] )
assume z in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis: ex b₁, b₂ being object st z = [b₁,b₂]
then ex x, y being Element of Day (R,A) st
( z = [x,y] & ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) ;
hence ex b₁, b₂ being object st z = [b₁,b₂] ; :: thesis: verum

end;

then reconsider RCC = R \/ { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } as Relation ;
take RCC ; :: thesis: ( R c= RCC & RCC preserves_No_Comparison_on ClosedProd (RCC,A,B) & RCC c= ClosedProd (RCC,A,B) )
thus R c= RCC by XBOOLE_1:7; :: thesis: ( RCC preserves_No_Comparison_on ClosedProd (RCC,A,B) & RCC c= ClosedProd (RCC,A,B) )
A2: R /\ [:(BeforeGames A),(BeforeGames A):] c= RCC /\ [:(BeforeGames A),(BeforeGames A):] by XBOOLE_1:7, XBOOLE_1:26;
A3: RCC /\ [:(BeforeGames A),(BeforeGames A):] c= R /\ [:(BeforeGames A),(BeforeGames A):]

proof

let y1, z1 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y1,z1] in RCC /\ [:(BeforeGames A),(BeforeGames A):] or [y1,z1] in R /\ [:(BeforeGames A),(BeforeGames A):] )
assume [y1,z1] in RCC /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: [y1,z1] in R /\ [:(BeforeGames A),(BeforeGames A):]
then A4: ( [y1,z1] in RCC & [y1,z1] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
not [y1,z1] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) }

proof

assume [y1,z1] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis: contradiction
then consider y, z being Element of Day (R,A) such that
A5: [y1,z1] = [y,z] and
A6: ( ( born (R,y) = B & born (R,z) = A ) or ( born (R,y) = A & born (R,z) = B ) ) and
( L_ y << R,{z} & {y} << R, R_ z ) ;
A7: ( y in BeforeGames A & z in BeforeGames A ) by A5, A4, ZFMISC_1:87;
then consider Oy being Ordinal such that
A8: ( Oy in A & y in Games Oy ) by Def5;
y in Day (R,Oy) by A8, Th12;
then A9: born (R,y) c= Oy by Def8;
consider Oz being Ordinal such that
A10: ( Oz in A & z in Games Oz ) by A7, Def5;
z in Day (R,Oz) by A10, Th12;
then born (R,z) c= Oz by Def8;
hence contradiction by A6, A9, A8, ORDINAL1:12, A10; :: thesis: verum

end;

then [y1,z1] in R by A4, XBOOLE_0:def 3;
hence [y1,z1] in R /\ [:(BeforeGames A),(BeforeGames A):] by A4, XBOOLE_0:def 4; :: thesis: verum

end;

A11: RCC c= ClosedProd (R,A,B)

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in RCC or [x,y] in ClosedProd (R,A,B) )
assume A12: [x,y] in RCC ; :: thesis: [x,y] in ClosedProd (R,A,B)

per cases ( [x,y] in R or [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ) by A12, XBOOLE_0:def 3;

suppose [x,y] in R ; :: thesis: [x,y] in ClosedProd (R,A,B)

then ( [x,y] in OpenProd (R,A,B) & OpenProd (R,A,B) c= ClosedProd (R,A,B) ) by A1, Th16;
hence [x,y] in ClosedProd (R,A,B) ; :: thesis: verum

end;

suppose [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis: [x,y] in ClosedProd (R,A,B)

then consider x1, y1 being Element of Day (R,A) such that
A13: [x,y] = [x1,y1] and
A14: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
thus [x,y] in ClosedProd (R,A,B) by A13, A14, Def10; :: thesis: verum

end;

end;

end;

RCC preserves_No_Comparison_on ClosedProd (R,A,B)

proof

let x, y be object ; :: according to SURREAL0:def 11 :: thesis: ( [x,y] in ClosedProd (R,A,B) implies ( x <= RCC,y iff ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ) )
assume A15: [x,y] in ClosedProd (R,A,B) ; :: thesis: ( x <= RCC,y iff ( L_ x << RCC,{y} & {x} << RCC, R_ y ) )
A16: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;

per cases ( [x,y] in OpenProd (R,A,B) or not [x,y] in OpenProd (R,A,B) ) ;

suppose A17: [x,y] in OpenProd (R,A,B) ; :: thesis: ( x <= RCC,y iff ( L_ x << RCC,{y} & {x} << RCC, R_ y ) )

thus ( x <= RCC,y implies ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ) :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y implies x <= RCC,y )

proof

assume x <= RCC,y ; :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y )

per cases then ( [x,y] in R or [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ) by XBOOLE_0:def 3;

suppose [x,y] in R ; :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y )

then x <= R,y ;
then A18: ( L_ x << R,{y} & {x} << R, R_ y ) by A1;
thus L_ x << RCC,{y} :: thesis: {x} << RCC, R_ y

proof

given l, r being object such that A19: ( l in L_ x & r in {y} & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A20: r = y by A19, TARSKI:def 1;
not l >= R,r by A19, A18;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A19, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A21: [r,l] = [x1,y1] and
A22: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A23: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;
then A24: x in Day (R,(born (R,x))) by Def8;
l in (L_ x) \/ (R_ x) by A19, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A25: ( Ol in born (R,x) & l in Day (R,Ol) ) by A24, Th7;
A26: ( r = x1 & l = y1 ) by A21, XTUPLE_0:1;
A27: born (R,l) c= Ol by A25, Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A17, A23, Def9;
hence contradiction by A27, A26, A25, A20, A22; :: thesis: verum

end;

thus {x} << RCC, R_ y :: thesis: verum

proof

given l, r being object such that A28: ( l in {x} & r in R_ y & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A29: l = x by A28, TARSKI:def 1;
not l >= R,r by A28, A18;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A28, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A30: [r,l] = [x1,y1] and
A31: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A32: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;
then A33: y in Day (R,(born (R,y))) by Def8;
r in (L_ y) \/ (R_ y) by A28, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A34: ( Or in born (R,y) & r in Day (R,Or) ) by A33, Th7;
A35: ( r = x1 & l = y1 ) by A30, XTUPLE_0:1;
A36: born (R,r) c= Or by A34, Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A17, A32, Def9;
hence contradiction by A36, A31, A35, A29, A34; :: thesis: verum

end;

end;

suppose [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y )

then consider x1, y1 being Element of Day (R,A) such that
A37: [x,y] = [x1,y1] and
A38: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
( ( not born (R,x1) in B or not born (R,y1) = A ) & ( not born (R,x1) = A or not born (R,y1) in B ) & ( not born (R,x1) in A or not born (R,y1) in A ) ) by A38;
hence ( L_ x << RCC,{y} & {x} << RCC, R_ y ) by A37, A17, Def9; :: thesis: verum

end;

end;

end;

assume A39: ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ; :: thesis: x <= RCC,y
A40: L_ x << R,{y}

proof

given l, r being object such that A41: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
l >= RCC,r by A41, XBOOLE_0:def 3;
hence contradiction by A39, A41; :: thesis: verum

end;

{x} << R, R_ y

proof

given l, r being object such that A42: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
l >= RCC,r by A42, XBOOLE_0:def 3;
hence contradiction by A39, A42; :: thesis: verum

end;

then x <= R,y by A17, A1, A40;
hence x <= RCC,y by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A43: not [x,y] in OpenProd (R,A,B) ; :: thesis: ( x <= RCC,y iff ( L_ x << RCC,{y} & {x} << RCC, R_ y ) )

then [x,y] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) by A15, XBOOLE_0:def 5;
then A44: ( ( born (R,x) = A & born (R,y) = B ) or ( born (R,x) = B & born (R,y) = A ) ) by Th25;
thus ( x <= RCC,y implies ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ) :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y implies x <= RCC,y )

proof

assume x <= RCC,y ; :: thesis: ( L_ x << RCC,{y} & {x} << RCC, R_ y )
then ( [x,y] in R or [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ) by XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A45: [x,y] = [x1,y1] and
A46: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
A47: ( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) by A1, A43;
A48: ( x = x1 & y = y1 ) by A45, XTUPLE_0:1;
thus L_ x << RCC,{y} :: thesis: {x} << RCC, R_ y

proof

given l, r being object such that A49: ( l in L_ x & r in {y} & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A50: r = y by A49, TARSKI:def 1;
not l >= R,r by A49, A47, A48;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A49, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A51: [r,l] = [x1,y1] and
A52: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A53: x in Day (R,(born (R,x))) by A16, Def8;
l in (L_ x) \/ (R_ x) by A49, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A54: ( Ol in born (R,x) & l in Day (R,Ol) ) by A53, Th7;
A55: ( r = x1 & l = y1 ) by A51, XTUPLE_0:1;
born (R,l) c= Ol by A54, Def8;
hence contradiction by A46, A48, A50, A52, A55, A54, ORDINAL1:12; :: thesis: verum

end;

thus {x} << RCC, R_ y :: thesis: verum

proof

given l, r being object such that A56: ( l in {x} & r in R_ y & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A57: l = x by A56, TARSKI:def 1;
not l >= R,r by A56, A47, A48;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A56, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A58: [r,l] = [x1,y1] and
A59: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A60: y in Day (R,(born (R,y))) by A16, Def8;
r in (L_ y) \/ (R_ y) by A56, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A61: ( Or in born (R,y) & r in Day (R,Or) ) by A60, Th7;
A62: ( r = x1 & l = y1 ) by A58, XTUPLE_0:1;
born (R,r) c= Or by A61, Def8;
hence contradiction by A46, A48, A57, A59, A62, A61, ORDINAL1:12; :: thesis: verum

end;

end;

assume A63: ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ; :: thesis: x <= RCC,y
A64: L_ x << R,{y}

proof

given l, r being object such that A65: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
l >= RCC,r by A65, XBOOLE_0:def 3;
hence contradiction by A63, A65; :: thesis: verum

end;

{x} << R, R_ y

proof

given l, r being object such that A66: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
l >= RCC,r by A66, XBOOLE_0:def 3;
hence contradiction by A63, A66; :: thesis: verum

end;

then [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A64, A44, A16;
hence x <= RCC,y by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence ( RCC preserves_No_Comparison_on ClosedProd (RCC,A,B) & RCC c= ClosedProd (RCC,A,B) ) by A3, Th15, A2, XBOOLE_0:def 10, A11; :: thesis: verum