let x be Surreal; :: thesis: ( ( for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) ) & x in born_eq_set x & (L_ x) \/ (R_ x) is uniq-surreal-membered implies x is uSurreal )
assume that
A1: for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) and
A2: ( x in born_eq_set x & (L_ x) \/ (R_ x) is uniq-surreal-membered ) ; :: thesis: x is uSurreal
set c = Unique_No x;
set B = born_eq x;
A3: Unique_No x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
A4: born_eq x in succ (born_eq x) by ORDINAL1:6;
x in Day (born_eq x) by A2, Def6;
then ( born x c= born_eq x & born_eq x c= born x ) by SURREAL0:def 18, Def5;
then A5: born x = born_eq x by XBOOLE_0:def 10;
A6: x == Unique_No x by Def10;
A7: ( born_eq (Unique_No x) = born_eq x & born_eq_set (Unique_No x) = born_eq_set x ) by Def10, Th33, Th34;
born_eq (Unique_No x) = born (Unique_No x) by A3, Th38;
then not Unique_No x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A3, Th38, A7;
then consider Y being non empty surreal-membered set such that
A8: ( Y = (born_eq_set (Unique_No x)) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & Unique_No x = the Y -smallest Surreal ) by A3, A4, Def9;
Unique_No x in Y by A8, Def7;
then A9: ( Unique_No x in born_eq_set x & (L_ (Unique_No x)) \/ (R_ (Unique_No x)) is uniq-surreal-membered ) by A7, A8, XBOOLE_0:def 4;
A10: x in born_eq_set (Unique_No x) by A2, Def10, Th34;
(L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x)))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (L_ x) \/ (R_ x) or o in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) )
assume A11: o in (L_ x) \/ (R_ x) ; :: thesis: o in union (rng ((unique_No_op (born_eq x)) | (born_eq x)))
then reconsider y = o as uSurreal by A2;
set C = born_eq y;
A12: born y = born_eq y by Th48;
y = Unique_No y by Def11;
then A13: y in (unique_No_op (born_eq y)) . (born_eq y) by Def10;
A14: born_eq y in born_eq x by A5, A12, A11, Th1;
born_eq y c= born_eq x by A5, A12, A11, Th1, ORDINAL1:def 2;
then A15: (unique_No_op (born_eq y)) . (born_eq y) = (unique_No_op (born_eq x)) . (born_eq y) by Th39;
A16: ((unique_No_op (born_eq x)) | (born_eq x)) . (born_eq y) = (unique_No_op (born_eq x)) . (born_eq y) by A5, A12, A11, Th1, FUNCT_1:49;
dom (unique_No_op (born_eq x)) = succ (born_eq x) by Def9;
then dom ((unique_No_op (born_eq x)) | (born_eq x)) = born_eq x by A4, RELAT_1:62, ORDINAL1:def 2;
then (unique_No_op (born_eq y)) . (born_eq y) in rng ((unique_No_op (born_eq x)) | (born_eq x)) by A15, A14, A16, FUNCT_1:def 3;
hence o in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A13, TARSKI:def 4; :: thesis: verum

end;

then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by Def8;
then x in Y by A8, A10, XBOOLE_0:def 4;
then (card (L_ (Unique_No x))) (+) (card (R_ (Unique_No x))) c= (card (L_ x)) (+) (card (R_ x)) by A8, A6, Def7;
hence x is uSurreal by A9, A1, ORDINAL1:5; :: thesis: verum