let A, B be Ordinal; :: thesis: for R, S being Relation st B c= A & R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,B) = Day (S,B)
let R, S be Relation; :: thesis: ( B c= A & R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] implies Day (R,B) = Day (S,B) )
assume that
A1: B c= A and
A2: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: Day (R,B) = Day (S,B)
BeforeGames B c= BeforeGames A by A1, Th5;
then A3: [:(BeforeGames B),(BeforeGames B):] /\ [:(BeforeGames A),(BeforeGames A):] = [:(BeforeGames B),(BeforeGames B):] by XBOOLE_1:28, ZFMISC_1:96;
then R /\ [:(BeforeGames B),(BeforeGames B):] = (S /\ [:(BeforeGames A),(BeforeGames A):]) /\ [:(BeforeGames B),(BeforeGames B):] by A2, XBOOLE_1:16
.= S /\ [:(BeforeGames B),(BeforeGames B):] by A3, XBOOLE_1:16 ;
hence Day (R,B) = Day (S,B) by Lm1; :: thesis: verum