theorem Th7: :: SURREAL0:7

for O being Ordinal
for R being Relation
for x being Element of Games O holds
( x in Day (R,O) iff ( L_ x << R, R_ x & ( for o being object st o in (L_ x) \/ (R_ x) holds
ex A being Ordinal st
( A in O & o in Day (R,A) ) ) ) )