:: deftheorem Def6 defines Day SURREAL0:def 6 :
for O being Ordinal
for R being Relation
for b₃ being Subset of (Games O) holds
( b₃ = Day (R,O) iff ex L being Sequence st
( b₃ = L . O & 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 ) } ) ) );