theorem Th51: :: SURREALO:51

for x, c being Surreal st born c = born_eq c & L_ c << {x} & {x} << R_ c holds
born c c= born x