theorem :: SURREALO:46

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 0 iff x = 0_No )