let R be Relation; :: thesis: Day (R,0) = Games 0
reconsider A = [{},{}] as Element of Games 0 by Th2, TARSKI:def 1;
A1: L_ A << R, R_ A ;
for x being object st x in (L_ A) \/ (R_ A) holds
ex O being Ordinal st
( O in 0 & x in Day (R,O) ) ;
then A in Day (R,0) by Th7, A1;
hence Day (R,0) = Games 0 by Th2, ZFMISC_1:33; :: thesis: verum