let o be object ; :: thesis: for x being Surreal st x is uSurreal & o in (L_ x) \/ (R_ x) holds
o is uSurreal
let x be Surreal; :: thesis: ( x is uSurreal & o in (L_ x) \/ (R_ x) implies o is uSurreal )
set B = born_eq x;
assume A1: ( x is uSurreal & o in (L_ x) \/ (R_ x) ) ; :: thesis: o is uSurreal
then x = Unique_No x by Def11;
then A2: x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
(L_ x) \/ (R_ x) is surreal-membered ;
then reconsider y = o as Surreal by A1;
A3: born_eq x in succ (born_eq x) by ORDINAL1:6;
A4: born_eq x = born x by A2, Th38;
then not x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A2, Th38;
then consider Y being non empty surreal-membered set such that
A5: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & x = the Y -smallest Surreal ) by A2, A3, Def9;
x in Y by A5, Def7;
then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by A5, XBOOLE_0:def 4;
then (L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by Def8;
then consider Z being set such that
A6: ( y in Z & Z in rng ((unique_No_op (born_eq x)) | (born_eq x)) ) by A1, TARSKI:def 4;
consider o being object such that
A7: ( o in dom ((unique_No_op (born_eq x)) | (born_eq x)) & ((unique_No_op (born_eq x)) | (born_eq x)) . o = Z ) by A6, FUNCT_1:def 3;
reconsider o = o as Ordinal by A7;
y in (unique_No_op (born_eq x)) . o by A6, A7, FUNCT_1:47;
then A8: ( born_eq y = born y & born y c= o & y in (unique_No_op (born_eq x)) . (born y) ) by Th38;
born y c= born_eq x by A4, A1, Th1, ORDINAL1:def 2;
then y in (unique_No_op (born y)) . (born y) by A8, Th39;
then Unique_No y = y by Def10, A8;
hence o is uSurreal by Def11; :: thesis: verum