theorem Th1: :: SURREALO:1

for x, y being Surreal st y in (L_ x) \/ (R_ x) holds
born y in born x