theorem :: SURREALO:52

for c, x being uSurreal st L_ c << {x} & {x} << R_ c & x <> c holds
born c in born x