theorem :: SURREALO:53

for x being Surreal st born x = born_eq x & not born x is limit_ordinal holds
ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) )