let x, y be Surreal; :: thesis: ( x = [{y},{}] & y < 0_No implies x == 0_No )
assume ( x = [{y},{}] & y < 0_No ) ; :: thesis: x == 0_No
then A1: ( L_ x << {0_No} & {0_No} << R_ x ) by SURREALO:21;
born 0_No = {} by SURREAL0:37;
then for z being Surreal st L_ x << {z} & {z} << R_ x holds
born 0_No c= born z ;
hence x == 0_No by SURREALO:16, A1; :: thesis: verum