:: deftheorem Def7 defines -smallest SURREALO:def 7 :
for A being non empty surreal-membered set
for x being Surreal holds
( x is A -smallest iff ( x in A & ( for y being Surreal st y in A & y == x holds
(card (L_ x)) (+) (card (R_ x)) c= (card (L_ y)) (+) (card (R_ y)) ) ) );