consider x being object such that
A1: x in A by XBOOLE_0:def 1;
reconsider x = x as Surreal by A1, SURREAL0:def 16;
defpred S₁[ Ordinal] means ex y being Surreal st
( y in A & y == x & (card (L_ y)) (+) (card (R_ y)) = A );
S₁[(card (L_ x)) (+) (card (R_ x))] by A1;
then A2: ex O being Ordinal st S₁[O] ;
consider O being Ordinal such that
A3: ( S₁[O] & ( for B being Ordinal st S₁[B] holds
O c= B ) ) from ORDINAL1:sch 1(A2);
consider y being Surreal such that
A4: ( y in A & y == x & (card (L_ y)) (+) (card (R_ y)) = O ) by A3;
for z being Surreal st z in A & z == y holds
(card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in A & z == y implies (card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z)) )
assume A5: ( z in A & z == y ) ; :: thesis: (card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z))
then z == x by A4, Th4;
hence (card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z)) by A5, A3, A4; :: thesis: verum

end;

hence ex b₁ being Surreal st b₁ is A -smallest by A4, Def7; :: thesis: verum