let A, B be Ordinal; :: thesis: for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
OpenProd (R,A,B) = OpenProd (S,A,B)
let R, S be Relation; :: thesis: ( R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] implies OpenProd (R,A,B) = OpenProd (S,A,B) )
assume A1: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: OpenProd (R,A,B) = OpenProd (S,A,B)
A2: Day (R,A) = Day (S,A) by A1, Th10;
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in OpenProd (R,A,B) or [x,y] in OpenProd (S,A,B) ) & ( not [x,y] in OpenProd (S,A,B) or [x,y] in OpenProd (R,A,B) ) )
thus ( [x,y] in OpenProd (R,A,B) implies [x,y] in OpenProd (S,A,B) ) :: thesis: ( not [x,y] in OpenProd (S,A,B) or [x,y] in OpenProd (R,A,B) )

proof

assume A3: [x,y] in OpenProd (R,A,B) ; :: thesis: [x,y] in OpenProd (S,A,B)
A4: ( x in Day (R,A) & y in Day (R,A) ) by A3, ZFMISC_1:87;
A5: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A4, Th11;
( ( 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 A3, A4, Def9;
hence [x,y] in OpenProd (S,A,B) by A4, A2, A5, Def9; :: thesis: verum

end;

assume A6: [x,y] in OpenProd (S,A,B) ; :: thesis: [x,y] in OpenProd (R,A,B)
A7: ( x in Day (S,A) & y in Day (S,A) ) by A6, ZFMISC_1:87;
A8: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A7, Th11;
( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) in B ) or ( born (S,x) in B & born (S,y) = A ) ) by A6, A7, Def9;
hence [x,y] in OpenProd (R,A,B) by A7, A2, A8, Def9; :: thesis: verum