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,B)) = S /\ (OpenProd (S,A,B)) holds
R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):]
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)) implies R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] )
assume that
A1: ( R is almost-No-order & S is almost-No-order ) and
A2: R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) ; :: thesis: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):]
consider R0 being Ordinal such that
A3: R c= [:(Day (R,R0)),(Day (R,R0)):] by A1;
consider S0 being Ordinal such that
A4: S c= [:(Day (S,S0)),(Day (S,S0)):] by A1;
let y, z be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] or [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] ) & ( not [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] or [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] ) )
thus ( [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] implies [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] ) :: thesis: ( not [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] or [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] )

proof

assume [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):]
then A5: ( [y,z] in R & [y,z] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
then A6: ( y in BeforeGames A & z in BeforeGames A ) by ZFMISC_1:87;
A7: ( y in Day (R,R0) & z in Day (R,R0) ) by A3, A5, ZFMISC_1:87;
( y in BeforeGames A & z in BeforeGames A ) by A5, ZFMISC_1:87;
then consider Ay being Ordinal such that
A8: ( Ay in A & y in Games Ay ) by Def5;
consider Az being Ordinal such that
A9: ( Az in A & z in Games Az ) by A6, Def5;
A10: ( Day (R,Ay) c= Day (R,A) & Day (R,Az) c= Day (R,A) ) by Th9, A8, A9, ORDINAL1:def 2;
A11: ( y in Day (R,Ay) & z in Day (R,Az) ) by A8, A7, A9, Th12;
then ( born (R,y) c= Ay & born (R,z) c= Az ) by Def8;
then A12: ( born (R,y) in A & born (R,z) in A ) by A8, A9, ORDINAL1:12;
[y,z] in OpenProd (R,A,B) by A10, A11, A12, Def9;
then [y,z] in R /\ (OpenProd (R,A,B)) by XBOOLE_0:def 4, A5;
then [y,z] in S by A2, XBOOLE_0:def 4;
hence [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] by A5, XBOOLE_0:def 4; :: thesis: verum

end;

assume [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):]
then A13: ( [y,z] in S & [y,z] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
then A14: ( y in BeforeGames A & z in BeforeGames A ) by ZFMISC_1:87;
A15: ( y in Day (S,S0) & z in Day (S,S0) ) by A4, A13, ZFMISC_1:87;
consider Ay being Ordinal such that
A16: ( Ay in A & y in Games Ay ) by A14, Def5;
consider Az being Ordinal such that
A17: ( Az in A & z in Games Az ) by A14, Def5;
A18: ( Day (S,Ay) c= Day (S,A) & Day (S,Az) c= Day (S,A) ) by Th9, A16, A17, ORDINAL1:def 2;
A19: ( y in Day (S,Ay) & z in Day (S,Az) ) by A16, A15, A17, Th12;
then ( born (S,y) c= Ay & born (S,z) c= Az ) by Def8;
then A20: ( born (S,y) in A & born (S,z) in A ) by A16, A17, ORDINAL1:12;
[y,z] in OpenProd (S,A,B) by A18, A19, A20, Def9;
then [y,z] in S /\ (OpenProd (S,A,B)) by XBOOLE_0:def 4, A13;
then [y,z] in R by A2, XBOOLE_0:def 4;
hence [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] by A13, XBOOLE_0:def 4; :: thesis: verum