let x, y be Surreal; :: thesis: ( x = [{y},{}] & born x is finite & 0_No <= y implies ex n being Nat st
( x == uInt . (n + 1) & uInt . n <= y & y < uInt . (n + 1) & n in born x ) )
assume A1: ( x = [{y},{}] & born x is finite & 0_No <= y ) ; :: thesis: ex n being Nat st
( x == uInt . (n + 1) & uInt . n <= y & y < uInt . (n + 1) & n in born x )
reconsider a = born x as Nat by A1;
defpred S₁[ Nat] means L_ x << {(uInt . $1)};
A2: x in Day a by SURREAL0:def 18;
L_ x << {x} by SURREALO:11;
then S₁[a] by A2, Th2, SURREALO:17;
then A3: ex k being Nat st S₁[k] ;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
k <> 0

proof

assume k = 0 ; :: thesis: contradiction
then {y} << {0_No} by Def1, A1, A4;
hence contradiction by A1, SURREALO:21; :: thesis: verum

end;

then reconsider k1 = k - 1 as Nat by NAT_1:20;
take k1 ; :: thesis: ( x == uInt . (k1 + 1) & uInt . k1 <= y & y < uInt . (k1 + 1) & k1 in born x )
A5: ( L_ x << {(uInt . k)} & {(uInt . k)} << R_ x ) by A4, A1;
for z being Surreal st L_ x << {z} & {z} << R_ x holds
born (uInt . k) c= born z

proof

let z be Surreal; :: thesis: ( L_ x << {z} & {z} << R_ x implies born (uInt . k) c= born z )
assume that
A6: ( L_ x << {z} & {z} << R_ x ) and
A7: not born (uInt . k) c= born z ; :: thesis: contradiction
A8: ( born z in born (uInt . k) & born (uInt . k) = k & k = Segm k ) by Th4, A7, ORDINAL1:16;
then reconsider bz = born z as Nat ;
( bz < k & k = k1 + 1 ) by A8, NAT_1:44;
then bz <= k1 by NAT_1:13;
then Segm bz c= Segm k1 by NAT_1:39;
then ( z in Day bz & Day bz c= Day k1 ) by SURREAL0:35, SURREAL0:def 18;
then L_ x << {(uInt . k1)} by Th2, A6, SURREALO:17;
then k1 + 1 <= k1 by A4;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence x == uInt . (k1 + 1) by A5, SURREALO:16; :: thesis: ( uInt . k1 <= y & y < uInt . (k1 + 1) & k1 in born x )
A9: uInt . k1 <= y

proof

assume y < uInt . k1 ; :: thesis: contradiction
then L_ x << {(uInt . k1)} by SURREALO:21, A1;
then k1 + 1 <= k1 by A4;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence ( uInt . k1 <= y & y < uInt . (k1 + 1) ) by SURREALO:21, A4, A1; :: thesis: k1 in born x
A10: k1 c= born y

proof

assume A11: not k1 c= born y ; :: thesis: contradiction
then k1 <> 0 ;
then reconsider k2 = k1 - 1 as Nat by NAT_1:20;
k1 = k2 + 1 ;
then Segm k1 = succ (Segm k2) by NAT_1:38;
then born y c= k2 by A11, ORDINAL1:16, ORDINAL1:22;
then ( y in Day (born y) & Day (born y) c= Day k2 ) by SURREAL0:35, SURREAL0:def 18;
then ( y <= uInt . k2 & uInt . k2 < uInt . (k2 + 1) ) by Th2, Lm1;
hence contradiction by A9, SURREALO:4; :: thesis: verum

end;

y in (L_ x) \/ (R_ x) by A1, TARSKI:def 1;
hence k1 in born x by SURREALO:1, A10, ORDINAL1:12; :: thesis: verum