theorem :: SURREALO:47

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 1 iff ex y being Surreal st
( x = [{},{y}] or x = [{y},{}] ) )