theorem Th16: :: SURREALO:16

for x, y being Surreal st L_ y << {x} & {x} << R_ y & ( for z being Surreal st L_ y << {z} & {z} << R_ y holds
born x c= born z ) holds
x == y