theorem Th6: :: SURREAL0:6

for O being Ordinal
for R being Relation
for L being Sequence st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) holds
for A being Ordinal st A in succ O holds
L . A = Day (R,A)