theorem :: SURREALO:49

for x being Surreal st ( for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) ) & x in born_eq_set x & (L_ x) \/ (R_ x) is uniq-surreal-membered holds
x is uSurreal