let x be Surreal; :: thesis: for n being Nat st x in Day n holds
ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )
let n be Nat; :: thesis: ( x in Day n implies ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n ) )
assume A1: x in Day n ; :: thesis: ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )
then A2: born x c= n by SURREAL0:def 18;

per cases ( ex i being Integer st x == uDyadic . i or for i being Integer holds not x == uDyadic . i ) ;

suppose ex i being Integer st x == uDyadic . i ; :: thesis: ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )

then consider i being Integer such that
A3: x == uDyadic . i ;
take i ; :: thesis: ( x == uDyadic . i & uDyadic . i in Day n )
born_eq_set x = born_eq_set (uDyadic . i) by A3, SURREALO:34;
then uDyadic . i in born_eq_set x by Th30;
then uDyadic . i in Day (born_eq x) by SURREALO:def 6;
then ( born (uDyadic . i) c= born_eq x & born_eq x c= born x ) by SURREAL0:def 18, SURREALO:def 5;
then born (uDyadic . i) c= born x by XBOOLE_1:1;
then born (uDyadic . i) c= n by A2, XBOOLE_1:1;
then ( uDyadic . i in Day (born (uDyadic . i)) & Day (born (uDyadic . i)) c= Day n ) by SURREAL0:def 18, SURREAL0:35;
hence ( x == uDyadic . i & uDyadic . i in Day n ) by A3; :: thesis: verum

end;

suppose A4: for i being Integer holds not x == uDyadic . i ; :: thesis: ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )

per cases ( 0_No <= x or x < 0_No ) ;

suppose A5: 0_No <= x ; :: thesis: ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )

not x == uDyadic . n by A4;
then consider x1, y1, p1 being Nat such that
A6: ( x == uDyadic . (x1 + (y1 / (2 |^ p1))) & y1 < 2 |^ p1 & x1 + p1 < n ) by A1, A5, Th25;
x1 + (y1 / (2 |^ p1)) is not Integer by A6, A4;
then consider n2, m2, p2 being Nat such that
A7: ( x1 + (y1 / (2 |^ p1)) = n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))) & (2 * m2) + 1 < 2 |^ (p2 + 1) ) by Th28;
take d = n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))); :: thesis: ( x == uDyadic . d & uDyadic . d in Day n )
A8: x1 = n2 by A6, A7, Th32;
then A9: n2 + (p2 + 1) <= n2 + p1 by Th34, A7, XREAL_1:6;
n2 + (p2 + 1) < n by A6, A8, A9, XXREAL_0:2;
then (n2 + (p2 + 1)) + 1 <= n by NAT_1:13;
then Segm ((n2 + (p2 + 1)) + 1) c= Segm n by NAT_1:39;
then A10: Day ((n2 + (p2 + 1)) + 1) c= Day n by SURREAL0:35;
born (uDyadic . d) = (n2 + (p2 + 1)) + 1 by Th26, A7;
then uDyadic . d in Day ((n2 + (p2 + 1)) + 1) by SURREAL0:def 18;
hence ( x == uDyadic . d & uDyadic . d in Day n ) by A10, A6, A7; :: thesis: verum

end;

suppose x < 0_No ; :: thesis: ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )

then A11: ( 0_No = - 0_No & - 0_No <= - x ) by SURREALR:10;
( born (- x) = born x & born x c= n ) by SURREAL0:def 18, A1, SURREALR:12;
then A12: ( - x in Day (born x) & Day (born x) c= Day n ) by SURREAL0:def 18, SURREAL0:35;
not - x == uDyadic . n

proof

assume - x == uDyadic . n ; :: thesis: contradiction
then ( - (- x) == - (uDyadic . n) & - (uDyadic . n) = uDyadic . (- n) ) by SURREALR:10, Th27;
hence contradiction by A4; :: thesis: verum

end;

then consider x1, y1, p1 being Nat such that
A13: ( - x == uDyadic . (x1 + (y1 / (2 |^ p1))) & y1 < 2 |^ p1 & x1 + p1 < n ) by A12, A11, Th25;
- (- x) == - (uDyadic . (x1 + (y1 / (2 |^ p1)))) by A13, SURREALR:10;
then x == uDyadic . (- (x1 + (y1 / (2 |^ p1)))) by Th27;
then - (- (x1 + (y1 / (2 |^ p1)))) is not Integer by A4;
then consider n2, m2, p2 being Nat such that
A14: ( x1 + (y1 / (2 |^ p1)) = n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))) & (2 * m2) + 1 < 2 |^ (p2 + 1) ) by Th28;
set d = n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1)));
A15: ( x = - (- x) & - (- x) == - (uDyadic . (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))))) & - (uDyadic . (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))))) = uDyadic . (- (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))))) ) by A13, A14, SURREALR:10, Th27;
A16: x1 = n2 by A13, A14, Th32;
then A17: n2 + (p2 + 1) <= n2 + p1 by A14, Th34, XREAL_1:6;
n2 + (p2 + 1) < n by A13, A16, A17, XXREAL_0:2;
then (n2 + (p2 + 1)) + 1 <= n by NAT_1:13;
then Segm ((n2 + (p2 + 1)) + 1) c= Segm n by NAT_1:39;
then A18: Day ((n2 + (p2 + 1)) + 1) c= Day n by SURREAL0:35;
( born (uDyadic . (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))))) = born (- (uDyadic . (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1)))))) & born (- (uDyadic . (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1)))))) = born (uDyadic . (- (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1)))))) ) by SURREALR:12, Th27;
then born (uDyadic . (- (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1)))))) = (n2 + (p2 + 1)) + 1 by Th26, A14;
then uDyadic . (- (n2 + (((2 * m2) + 1) / (2 |^ (p2 + 1))))) in Day ((n2 + (p2 + 1)) + 1) by SURREAL0:def 18;
hence ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n ) by A15, A18; :: thesis: verum

end;

end;

end;

end;