let r be Real; :: thesis: for x being Surreal st x = [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] holds
x == uReal . r
let a be Surreal; :: thesis: ( a = [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] implies a == uReal . r )
assume A1: a = [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] ; :: thesis: a == uReal . r
A2: ( sReal . r == Unique_No (sReal . r) & Unique_No (sReal . r) = uReal . r ) by SURREALO:def 10, SURREALN:def 7;
L_ a << {(uReal . r)}

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in L_ a or not y in {(uReal . r)} or not y <= x )
assume A3: ( x in L_ a & y in {(uReal . r)} ) ; :: thesis: not y <= x
consider e1 being positive Real such that
A4: x = uReal . (r - e1) by A3, A1;
y = uReal . r by A3, TARSKI:def 1;
hence not y <= x by A4, XREAL_1:44, SURREALN:51; :: thesis: verum

end;

then A5: L_ a << {(sReal . r)} by A2, SURREALO:17;
{(uReal . r)} << R_ a

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in {(uReal . r)} or not y in R_ a or not y <= x )
assume A6: ( x in {(uReal . r)} & y in R_ a ) ; :: thesis: not y <= x
consider e1 being positive Real such that
A7: y = uReal . (r + e1) by A6, A1;
x = uReal . r by A6, TARSKI:def 1;
hence not y <= x by A7, XREAL_1:29, SURREALN:51; :: thesis: verum

end;

then A8: {(sReal . r)} << R_ a by A2, SURREALO:18;
A9: sReal . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] by SURREALN:def 6;
A10: L_ (sReal . r) << {a}

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in L_ (sReal . r) or not y in {a} or not y <= x )
assume A11: ( x in L_ (sReal . r) & y in {a} ) ; :: thesis: not y <= x
consider n being Nat such that
A12: x = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) by A11, A9;
reconsider R = r - ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) as positive Real by XREAL_1:50, SURREALN:41;
( x = uReal . (r - R) & uReal . (r - R) in L_ a & L_ a << {a} ) by A1, A12, SURREALN:46, SURREALO:11;
hence not y <= x by A11; :: thesis: verum

end;

A13: {a} << R_ (sReal . r)

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in {a} or not y in R_ (sReal . r) or not y <= x )
assume A14: ( x in {a} & y in R_ (sReal . r) ) ; :: thesis: not y <= x
consider n being Nat such that
A15: y = uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) by A14, A9;
reconsider R = ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) - r as positive Real by SURREALN:41, XREAL_1:50;
( y = uReal . (r + R) & uReal . (r + R) in R_ a & {a} << R_ a ) by A1, A15, SURREALN:46, SURREALO:11;
hence not y <= x by A14; :: thesis: verum

end;

( sReal . r <= a & a <= sReal . r ) by A10, A8, A5, A13, SURREAL0:43;
hence a == uReal . r by A2, SURREALO:9; :: thesis: verum