let A be Ordinal; :: thesis: for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
for a being object st a in Day (R,A) holds
born (R,a) = born (S,a)
let R, S be Relation; :: thesis: ( R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] implies for a being object st a in Day (R,A) holds
born (R,a) = born (S,a) )
assume A1: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: for a being object st a in Day (R,A) holds
born (R,a) = born (S,a)
A2: Day (R,A) = Day (S,A) by A1, Th10;
let x be object ; :: thesis: ( x in Day (R,A) implies born (R,x) = born (S,x) )
assume A3: x in Day (R,A) ; :: thesis: born (R,x) = born (S,x)
A4: x in Day (S,A) by A3, A1, Th10;
born (R,x) c= A by A3, Def8;
then Day (R,(born (R,x))) = Day (S,(born (R,x))) by A1, Th10;
then x in Day (S,(born (R,x))) by A3, Def8;
then A5: born (S,x) c= born (R,x) by Def8;
born (S,x) c= A by A3, A2, Def8;
then Day (S,(born (S,x))) = Day (R,(born (S,x))) by A1, Th10;
then x in Day (R,(born (S,x))) by A4, Def8;
then born (R,x) c= born (S,x) by Def8;
hence born (R,x) = born (S,x) by A5, XBOOLE_0:def 10; :: thesis: verum