let x be Surreal; :: thesis: ( (card (L_ x)) (+) (card (R_ x)) = 0 iff x = 0_No )

hereby :: thesis: ( x = 0_No implies (card (L_ x)) (+) (card (R_ x)) = 0 )

assume (card (L_ x)) (+) (card (R_ x)) = 0 ; :: thesis: x = 0_No
then ( L_ x = {} & R_ x = {} ) ;
hence x = 0_No ; :: thesis: verum

end;

thus ( x = 0_No implies (card (L_ x)) (+) (card (R_ x)) = 0 ) ; :: thesis: verum