let s, N, x be Surreal; :: thesis: for r being Real st x = [ { (s + ((uReal . (r - e1)) * N)) where e1 is positive Real : verum } , { (s + ((uReal . (r + e2)) * N)) where e2 is positive Real : verum } ] holds
( x is s,N,r _Term & ( for u1, u2 being uSurreal st u1 == x & u1 <> u2 & u2 is s,N,r _Term holds
born u1 in born u2 ) )
let r be Real; :: thesis: ( x = [ { (s + ((uReal . (r - e1)) * N)) where e1 is positive Real : verum } , { (s + ((uReal . (r + e2)) * N)) where e2 is positive Real : verum } ] implies ( x is s,N,r _Term & ( for u1, u2 being uSurreal st u1 == x & u1 <> u2 & u2 is s,N,r _Term holds
born u1 in born u2 ) ) )
assume A1: x = [ { (s + ((uReal . (r - e)) * N)) where e is positive Real : verum } , { (s + ((uReal . (r + e)) * N)) where e is positive Real : verum } ] ; :: thesis: ( x is s,N,r _Term & ( for u1, u2 being uSurreal st u1 == x & u1 <> u2 & u2 is s,N,r _Term holds
born u1 in born u2 ) )
|.(x - (s + ((uReal . r) * N))).| infinitely< N

proof

let t be positive Real; :: according to SURREALC:def 3 :: thesis: not N <= |.(x - (s + ((uReal . r) * N))).| * (uReal . t)
set T = 1 / t;
A2: s + ((uReal . (r + (1 / t))) * N) == (s + ((uReal . r) * N)) + ((uReal . (1 / t)) * N) by Th30;
A3: ( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
s + ((uReal . (r + (1 / t))) * N) in R_ x by A1;
then x < (s + ((uReal . r) * N)) + ((uReal . (1 / t)) * N) by A3, A2, SURREALO:9;
then A4: x - (s + ((uReal . r) * N)) < (uReal . (1 / t)) * N by SURREALR:41;
A5: s + ((uReal . (r - (1 / t))) * N) == (s + ((uReal . r) * N)) - ((uReal . (1 / t)) * N) by Th30;
A6: ( x in {x} & L_ x << {x} ) by TARSKI:def 1, SURREALO:11;
s + ((uReal . (r - (1 / t))) * N) in L_ x by A1;
then x > (s + ((uReal . r) * N)) - ((uReal . (1 / t)) * N) by A5, A6, SURREALO:9;
then ( x - (s + ((uReal . r) * N)) > - ((uReal . (1 / t)) * N) & - ((uReal . (1 / t)) * N) = - ((uReal . (1 / t)) * N) ) by SURREALR:42;
then A7: |.(x - (s + ((uReal . r) * N))).| < N * (uReal . (1 / t)) by A4, SURREALC:52;
A8: 0_No < uReal . t by SURREALN:47, SURREALN:51;
(1 / t) * t = 1 by XCMPLX_1:87;
then ( (N * (uReal . (1 / t))) * (uReal . t) == N * ((uReal . (1 / t)) * (uReal . t)) & N * ((uReal . (1 / t)) * (uReal . t)) == N * 1_No ) by SURREALR:54, SURREALR:69, SURREALN:57, SURREALN:48;
then A9: (N * (uReal . (1 / t))) * (uReal . t) == N by SURREALO:9;
|.(x - (s + ((uReal . r) * N))).| * (uReal . t) < (N * (uReal . (1 / t))) * (uReal . t) by A8, A7, SURREALR:70;
hence not N <= |.(x - (s + ((uReal . r) * N))).| * (uReal . t) by A9, SURREALO:9; :: thesis: verum

end;

hence x is s,N,r _Term by SURREALC:def 14; :: thesis: for u1, u2 being uSurreal st u1 == x & u1 <> u2 & u2 is s,N,r _Term holds
born u1 in born u2
let u1, u2 be uSurreal; :: thesis: ( u1 == x & u1 <> u2 & u2 is s,N,r _Term implies born u1 in born u2 )
assume A10: ( u1 == x & u1 <> u2 & u2 is s,N,r _Term ) ; :: thesis: born u1 in born u2
A11: not u1 == u2 by A10, SURREALO:50;
Unique_No x == x by SURREALO:def 10;
then Unique_No x == u1 by A10, SURREALO:9;
then A12: Unique_No x = u1 by SURREALO:50;
A13: not x == u2 by A10, A11, SURREALO:9;
( L_ x << {u2} & {u2} << R_ x )

proof

thus L_ x << {u2} :: thesis: {u2} << R_ x

proof

let l, r1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ x or not r1 in {u2} or not r1 <= l )
assume A14: ( l in L_ x & r1 in {u2} ) ; :: thesis: not r1 <= l
consider e being positive Real such that
A15: l = s + ((uReal . (r - e)) * N) by A1, A14;
set E = e;
r1 is s,N,r _Term by A10, A14, TARSKI:def 1;
then |.(r1 - (s + ((uReal . r) * N))).| infinitely< N by SURREALC:def 14;
then |.(r1 - (s + ((uReal . r) * N))).| infinitely< N * (uReal . e) by SURREALC:13;
then |.(r1 - (s + ((uReal . r) * N))).| < N * (uReal . e) by SURREALC:9;
then r1 - (s + ((uReal . r) * N)) > - (N * (uReal . e)) by SURREALC:52;
then A16: r1 > (s + ((uReal . r) * N)) + (- (N * (uReal . e))) by SURREALR:42;
s + ((uReal . (r - e)) * N) == (s + ((uReal . r) * N)) - ((uReal . e) * N) by Th30;
hence l < r1 by A15, A16, SURREALO:9; :: thesis: verum

end;

let l1, r1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l1 in {u2} or not r1 in R_ x or not r1 <= l1 )
assume A17: ( l1 in {u2} & r1 in R_ x ) ; :: thesis: not r1 <= l1
consider e being positive Real such that
A18: r1 = s + ((uReal . (r + e)) * N) by A1, A17;
set E = e;
l1 is s,N,r _Term by A10, A17, TARSKI:def 1;
then |.(l1 - (s + ((uReal . r) * N))).| infinitely< N by SURREALC:def 14;
then |.(l1 - (s + ((uReal . r) * N))).| infinitely< N * (uReal . e) by SURREALC:13;
then |.(l1 - (s + ((uReal . r) * N))).| < N * (uReal . e) by SURREALC:9;
then l1 - (s + ((uReal . r) * N)) < N * (uReal . e) by SURREALC:52;
then A19: l1 < (s + ((uReal . r) * N)) + (N * (uReal . e)) by SURREALR:41;
s + ((uReal . (r + e)) * N) == (s + ((uReal . r) * N)) + ((uReal . e) * N) by Th30;
hence l1 < r1 by A18, A19, SURREALO:9; :: thesis: verum

end;

hence born u1 in born u2 by A12, Th53, A13; :: thesis: verum