theorem Th15: :: SURREALO:15

for x, y, z being Surreal st L_ y << {x} & {x} << R_ y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] holds
x == z