theorem Th4: :: SURREAL0:4

for O being Ordinal
for o being object holds
( o in Games O iff ( o is pair & ( for a being object st a in (L_ o) \/ (R_ o) holds
ex A being Ordinal st
( A in O & a in Games A ) ) ) )