let d be Dyadic; :: thesis: ( sReal . d == uDyadic . d & uDyadic . d = uReal . d )
set Rd = sReal . d;
set Dd = uDyadic . d;
consider i being Integer, k being Nat such that
A1: d = i / (2 |^ k) by Th18;
A2: ( L_ (sReal . d) << {(uDyadic . d)} & {(uDyadic . d)} << R_ (sReal . d) )

proof

thus L_ (sReal . d) << {(uDyadic . d)} :: thesis: {(uDyadic . d)} << R_ (sReal . d)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L_ (sReal . d) or not r in {(uDyadic . d)} or not r <= l )
assume A3: ( l in L_ (sReal . d) & r in {(uDyadic . d)} ) ; :: thesis: not r <= l
consider n being Nat such that
A4: l = uDyadic . ([/((d * (2 |^ n)) - 1)\] / (2 |^ n)) by A3, Th42;
l < uDyadic . d by Th41, A4, Th24;
hence not r <= l by A3, TARSKI:def 1; :: thesis: verum

end;

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in {(uDyadic . d)} or not r in R_ (sReal . d) or not r <= l )
assume A5: ( l in {(uDyadic . d)} & r in R_ (sReal . d) ) ; :: thesis: not r <= l
consider n being Nat such that
A6: r = uDyadic . ([\((d * (2 |^ n)) + 1)/] / (2 |^ n)) by A5, Th43;
uDyadic . d < r by Th41, A6, Th24;
hence not r <= l by A5, TARSKI:def 1; :: thesis: verum

end;

for z being Surreal st L_ (sReal . d) << {z} & {z} << R_ (sReal . d) holds
born (uDyadic . d) c= born z

proof

born (uDyadic . d) is finite by Th37;
then reconsider B = born (uDyadic . d) as Nat ;
let z be Surreal; :: thesis: ( L_ (sReal . d) << {z} & {z} << R_ (sReal . d) implies born (uDyadic . d) c= born z )
assume A7: ( L_ (sReal . d) << {z} & {z} << R_ (sReal . d) ) ; :: thesis: born (uDyadic . d) c= born z
assume A8: not born (uDyadic . d) c= born z ; :: thesis: contradiction
then born z in Segm B by ORDINAL1:16;
then reconsider Z = born z as Nat ;
z in Day Z by SURREAL0:def 18;
then consider f being Dyadic such that
A9: ( z == uDyadic . f & uDyadic . f in Day Z ) by Th35;
consider j being Integer, m being Nat such that
A10: f = j / (2 |^ m) by Th18;
set F = uDyadic . f;
A11: ( L_ (sReal . d) << {(uDyadic . f)} & uDyadic . f in {(uDyadic . f)} & {(uDyadic . f)} << R_ (sReal . d) ) by A7, A9, SURREALO:17, SURREALO:18, TARSKI:def 1;
(m + k) + 1 = k + (m + 1) ;
then 2 |^ ((m + k) + 1) = (2 |^ k) * (2 |^ (m + 1)) by NEWTON:8
.= (2 |^ k) * (2 * (2 |^ m)) by NEWTON:6 ;
then A12: d * (2 |^ ((m + k) + 1)) = (d * (2 |^ k)) * (2 * (2 |^ m))
.= i * (2 * (2 |^ m)) by A1, XCMPLX_1:87 ;

per cases ( f < d or d < f or d = f ) by XXREAL_0:1;

suppose f < d ; :: thesis: contradiction

then ( f < (((j * (2 |^ k)) * 2) + 1) / (2 |^ ((m + k) + 1)) & (((j * (2 |^ k)) * 2) + 1) / (2 |^ ((m + k) + 1)) <= (((i * (2 |^ m)) * 2) - 1) / (2 |^ ((m + k) + 1)) ) by Th45, A10, A1;
then A13: f < (((i * (2 |^ m)) * 2) - 1) / (2 |^ ((m + k) + 1)) by XXREAL_0:2;
[/((d * (2 |^ ((m + k) + 1))) - 1)\] = (i * (2 * (2 |^ m))) - 1 by A12;
then uDyadic . ((((i * (2 |^ m)) * 2) - 1) / (2 |^ ((m + k) + 1))) <= uDyadic . f by A11, Th42;
hence contradiction by A13, Th24; :: thesis: verum

end;

suppose d < f ; :: thesis: contradiction

then ( (((i * (2 |^ m)) * 2) + 1) / (2 |^ ((m + k) + 1)) <= (((j * (2 |^ k)) * 2) - 1) / (2 |^ ((m + k) + 1)) & (((j * (2 |^ k)) * 2) - 1) / (2 |^ ((m + k) + 1)) < f ) by Th45, A10, A1;
then A14: (((i * (2 |^ m)) * 2) + 1) / (2 |^ ((m + k) + 1)) < f by XXREAL_0:2;
[\((d * (2 |^ ((m + k) + 1))) + 1)/] = (i * (2 * (2 |^ m))) + 1 by A12;
then uDyadic . f <= uDyadic . ((((i * (2 |^ m)) * 2) + 1) / (2 |^ ((m + k) + 1))) by A11, Th43;
hence contradiction by A14, Th24; :: thesis: verum

end;

suppose d = f ; :: thesis: contradiction

hence contradiction by A9, SURREAL0:def 18, A8; :: thesis: verum

end;

end;

end;

hence A15: sReal . d == uDyadic . d by A2, SURREALO:16; :: thesis: uDyadic . d = uReal . d
uReal . d = Unique_No (sReal . d) by Def7;
then sReal . d == uReal . d by SURREALO:def 10;
then uReal . d == uDyadic . d by A15, SURREALO:4;
hence uDyadic . d = uReal . d by SURREALO:50; :: thesis: verum