defpred S₁[ Nat] means ( ( for d being Dyadic st uDyadic . d in Day d holds
uDyadic . d is uniq-surreal ) & ( for x being Surreal st x in Day d & x is uniq-surreal holds
- x is uniq-surreal ) );
A1: S₁[ 0 ] by SURREALR:23, SURREAL0:2, TARSKI:def 1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
thus A4: for d being Dyadic st uDyadic . d in Day (n + 1) holds
uDyadic . d is uniq-surreal :: thesis: for x being Surreal st x in Day (n + 1) & x is uniq-surreal holds
- x is uniq-surreal

proof

A5: for d being Dyadic st 0 <= d & d is not Integer & uDyadic . d in (Day (n + 1)) \ (Day n) holds
( ( for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . d in born_eq_set (uDyadic . d) & (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered )

proof

let d be Dyadic; :: thesis: ( 0 <= d & d is not Integer & uDyadic . d in (Day (n + 1)) \ (Day n) implies ( ( for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . d in born_eq_set (uDyadic . d) & (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered ) )
set D = uDyadic . d;
assume that
A6: ( 0 <= d & d is not Integer ) and
A7: uDyadic . d in (Day (n + 1)) \ (Day n) ; :: thesis: ( ( for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . d in born_eq_set (uDyadic . d) & (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered )
A8: ( uDyadic . d in Day (n + 1) & not uDyadic . d in Day n ) by A7, XBOOLE_0:def 5;
not born (uDyadic . d) c= n

proof

assume born (uDyadic . d) c= n ; :: thesis: contradiction
then ( uDyadic . d in Day (born (uDyadic . d)) & Day (born (uDyadic . d)) c= Day n ) by SURREAL0:def 18, SURREAL0:35;
hence contradiction by A7, XBOOLE_0:def 5; :: thesis: verum

end;

then A9: ( Segm (n + 1) = succ (Segm n) & succ (Segm n) c= born (uDyadic . d) & born (uDyadic . d) c= n + 1 ) by A8, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18, NAT_1:38;
consider k, m, p being Nat such that
A10: ( d = k + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) ) by A6, Th28;
set p1 = p + 1;
A11: 2 |^ (p + 1) = 2 * (2 |^ p) by NEWTON:6;
then (k * (2 |^ (p + 1))) + ((2 * m) + 1) = (2 * ((k * (2 |^ p)) + m)) + 1 ;
then d = ((2 * ((k * (2 |^ p)) + m)) + 1) / (2 |^ (p + 1)) by A10, XCMPLX_1:113;
then A12: uDyadic . d = [{(uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)))},{(uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)))}] by Def5;
then ( card (L_ (uDyadic . d)) = 1 & card (R_ (uDyadic . d)) = 1 ) by CARD_1:30;
then A13: (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) = 1 + 1 by ORDINAL7:76;
A14: born (uDyadic . d) = (k + (p + 1)) + 1 by A10, Th26;
A15: m < 2 |^ p by XREAL_1:64, NAT_1:13, A11, A10;
A16: ((k * (2 |^ p)) + m) / (2 |^ p) = k + (m / (2 |^ p)) by XCMPLX_1:113;
A17: ( (((k * (2 |^ p)) + m) + 1) / (2 |^ p) = ((k * (2 |^ p)) + (m + 1)) / (2 |^ p) & ((k * (2 |^ p)) + (m + 1)) / (2 |^ p) = k + ((m + 1) / (2 |^ p)) ) by XCMPLX_1:113;
set sD1 = uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p));
set sD2 = uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p));
A18: 0_No <= uDyadic . d by A6, Th29;
A19: for y being Surreal st y == uDyadic . d holds
born (uDyadic . d) c= born y

proof

let y be Surreal; :: thesis: ( y == uDyadic . d implies born (uDyadic . d) c= born y )
assume A20: ( y == uDyadic . d & not born (uDyadic . d) c= born y ) ; :: thesis: contradiction
A21: born y in Segm ((k + (p + 1)) + 1) by A14, A20, ORDINAL1:16;
reconsider By = born y as Nat by A14, A20;
By < (k + (p + 1)) + 1 by A21, NAT_1:44;
then By <= k + (p + 1) by NAT_1:13;
then Segm By c= Segm (k + (p + 1)) by NAT_1:39;
then A22: ( y in Day By & Day By c= Day (k + (p + 1)) ) by SURREAL0:def 18, SURREAL0:35;
A23: not y == uDyadic . (k + (p + 1))

proof

assume y == uDyadic . (k + (p + 1)) ; :: thesis: contradiction
then ( d <= k + (p + 1) & k + (p + 1) <= d ) by Th24, A20, SURREALO:4;
hence contradiction by A6, XXREAL_0:1; :: thesis: verum

end;

consider x2, y2, p2 being Nat such that
A24: ( y == uDyadic . (x2 + (y2 / (2 |^ p2))) & y2 < 2 |^ p2 & x2 + p2 < k + (p + 1) ) by Th25, A22, A20, A18, SURREALO:4, A23;
( d <= x2 + (y2 / (2 |^ p2)) & x2 + (y2 / (2 |^ p2)) <= d ) by Th24, A20, A24, SURREALO:4;
then A25: k + (((2 * m) + 1) / (2 |^ (p + 1))) = x2 + (y2 / (2 |^ p2)) by A10, XXREAL_0:1;
then k = x2 by Th32, A10, A24;
hence contradiction by A25, Th34, A24, XREAL_1:6; :: thesis: verum

end;

then A26: born (uDyadic . d) = born_eq (uDyadic . d) by SURREALO:def 5;
then A27: uDyadic . d in Day (born_eq (uDyadic . d)) by SURREAL0:def 18;
( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) in L_ (uDyadic . d) & uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) in R_ (uDyadic . d) ) by TARSKI:def 1, A12;
then ( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) in (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) & uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) in (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) ) by XBOOLE_0:def 3;
then A28: ( born (uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p))) in born (uDyadic . d) & born (uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p))) in born (uDyadic . d) ) by SURREALO:1;
( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) in Day (born (uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)))) & Day (born (uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)))) c= Day n & uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) in Day (born (uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)))) & Day (born (uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)))) c= Day n ) by SURREAL0:def 18, SURREAL0:35, A28, A9, ORDINAL1:22;
then A29: ( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) is uniq-surreal & uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) is uniq-surreal ) by A3;
for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z implies (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) )
assume that
A30: ( z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z ) and
A31: not (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ; :: thesis: contradiction
A32: (card (L_ z)) (+) (card (R_ z)) c= (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) by A31, ORDINAL1:16;
A33: z == uDyadic . d by A30, SURREALO:def 6;
z in Day (born_eq (uDyadic . d)) by A30, SURREALO:def 6;
then A34: ( born z c= born_eq (uDyadic . d) & born_eq (uDyadic . d) c= born (uDyadic . d) ) by SURREAL0:def 18, SURREALO:def 5;
then A35: born z c= Segm ((k + (p + 1)) + 1) by A14, XBOOLE_1:1;
0_No <= uDyadic . d by A6, Th29;
then A36: 0_No <= z by A33, SURREALO:4;

per cases ( (card (L_ z)) (+) (card (R_ z)) <> 2 or (card (L_ z)) (+) (card (R_ z)) = 2 ) ;

suppose (card (L_ z)) (+) (card (R_ z)) <> 2 ; :: thesis: contradiction

then (card (L_ z)) (+) (card (R_ z)) in succ 1 by ORDINAL1:11, A32, A13, XBOOLE_0:def 8;
then consider i being Integer such that
A37: z == uInt . i by A34, A14, Th31, ORDINAL1:22;
( uDyadic . d == uInt . i & uInt . i = uDyadic . i ) by A33, A37, SURREALO:4, Def5;
then ( d <= i & i <= d ) by Th24;
hence contradiction by XXREAL_0:1, A6; :: thesis: verum

end;

suppose A38: (card (L_ z)) (+) (card (R_ z)) = 2 ; :: thesis: contradiction

( L_ z is finite & R_ z is finite ) by A34, A14, SURREALO:8;
then reconsider cz1 = card (L_ z), cz2 = card (R_ z) as Nat ;
A39: cz1 + cz2 = 2 by A38, ORDINAL7:76;
A40: cz1 = 1

proof

assume A41: cz1 <> 1 ; :: thesis: contradiction

per cases ( cz1 <> 0 or card (L_ z) = 0 ) ;

suppose A42: cz1 <> 0 ; :: thesis: contradiction

then 0 + 1 <= cz1 by NAT_1:13;
then 1 < cz1 by A41, XXREAL_0:1;
then ( 1 + 1 <= cz1 & cz1 <= cz1 + cz2 ) by NAT_1:13, NAT_1:11;
then A43: cz1 = 2 by A39, XXREAL_0:1;
( not L_ z is empty & L_ z is surreal-membered & L_ z is finite ) by A42;
then consider Min, Max being Surreal such that
A44: ( Min in L_ z & Max in L_ z & ( for x being Surreal st x in L_ z holds
( Min <= x & x <= Max ) ) ) by SURREALO:12;
A45: for x being Surreal st x in L_ z holds
x <= Max by A44;
then reconsider zM = [{Max},(R_ z)] as Surreal by A44, SURREALO:23;
A46: born zM c= born z by A44, A45, SURREALO:23;
A47: zM == z by A44, SURREALO:23, A45;
( (card (L_ zM)) (+) (card (R_ zM)) = 1 (+) 0 & 1 (+) 0 = 1 ) by A39, A43, CARD_1:30;
then consider i being Integer such that
A48: zM == uInt . i by A46, A34, A14, Th31;
z == uDyadic . d by A30, SURREALO:def 6;
then uDyadic . d == zM by A47, SURREALO:4;
then ( uDyadic . d == uInt . i & uInt . i = uDyadic . i ) by A48, SURREALO:4, Def5;
then ( d <= i & i <= d ) by Th24;
hence contradiction by A6, XXREAL_0:1; :: thesis: verum

end;

suppose A49: card (L_ z) = 0 ; :: thesis: contradiction

then ( not R_ z is empty & R_ z is surreal-membered & R_ z is finite ) by A38, ORDINAL7:69;
then consider Min, Max being Surreal such that
A50: ( Min in R_ z & Max in R_ z & ( for x being Surreal st x in R_ z holds
( Min <= x & x <= Max ) ) ) by SURREALO:12;
A51: for x being Surreal st x in R_ z holds
Min <= x by A50;
then reconsider zM = [(L_ z),{Min}] as Surreal by A50, SURREALO:24;
A52: born zM c= born z by A50, A51, SURREALO:24;
A53: zM == z by A50, SURREALO:24, A51;
( (card (L_ zM)) (+) (card (R_ zM)) = 0 (+) 1 & 0 (+) 1 = 1 ) by CARD_1:30, A49;
then consider i being Integer such that
A54: zM == uInt . i by A52, A34, A14, Th31;
z == uDyadic . d by A30, SURREALO:def 6;
then uDyadic . d == zM by A53, SURREALO:4;
then ( uDyadic . d == uInt . i & uInt . i = uDyadic . i ) by A54, SURREALO:4, Def5;
then ( d <= i & i <= d ) by Th24;
hence contradiction by A6, XXREAL_0:1; :: thesis: verum

end;

end;

end;

then consider Z1 being object such that
A55: L_ z = {Z1} by CARD_2:42;
consider Z2 being object such that
A56: R_ z = {Z2} by A40, A39, CARD_2:42;
A57: ( Z1 in L_ z & Z2 in R_ z ) by A55, A56, TARSKI:def 1;
then reconsider Z1 = Z1, Z2 = Z2 as Surreal by SURREAL0:def 16;
A58: ( Z1 in (L_ z) \/ (R_ z) & Z2 in (L_ z) \/ (R_ z) ) by A57, XBOOLE_0:def 3;
then reconsider Z1 = Z1, Z2 = Z2 as uSurreal by A30;
A59: ( {Z1} << {(uDyadic . d)} & {(uDyadic . d)} << {Z2} ) by A33, A55, A56, SURREAL0:43;
( born Z1 in born z & born Z2 in born z ) by A58, SURREALO:1;
then ( born Z1 in Segm ((k + (p + 1)) + 1) & born Z2 in Segm ((k + (p + 1)) + 1) & Segm ((k + (p + 1)) + 1) = succ (Segm (k + (p + 1))) ) by A35, NAT_1:38;
then A60: ( Z1 in Day (born Z1) & Z2 in Day (born Z2) & Day (born Z1) c= Day (k + (p + 1)) & Day (born Z2) c= Day (k + (p + 1)) ) by ORDINAL1:22, SURREAL0:35, SURREAL0:def 18;
A61: ( born z = born_eq z & born_eq z = born_eq (uDyadic . d) ) by A30, SURREALO:35;
A62: not Z1 == uDyadic . (k + (p + 1))

proof

assume Z1 == uDyadic . (k + (p + 1)) ; :: thesis: contradiction
then uDyadic . (k + (p + 1)) < uDyadic . d by A59, SURREALO:21, SURREALO:4;
then ( p + 1 < ((2 * m) + 1) / (2 |^ (p + 1)) & ((2 * m) + 1) / (2 |^ (p + 1)) < 1 ) by A10, Th24, XREAL_1:6, XREAL_1:189;
then p + 1 < 1 by XXREAL_0:2;
hence contradiction by NAT_1:11; :: thesis: verum

end;

A63: {0_No} << R_ z by A36, SURREAL0:43;
0_No <= Z1

proof

assume A64: not 0_No <= Z1 ; :: thesis: contradiction
born 0_No = {} by SURREAL0:37;
then for x being Surreal st L_ z << {x} & {x} << R_ z holds
born 0_No c= born x ;
then z == 0_No by A63, A64, A55, SURREALO:21, SURREALO:16;
then ( uDyadic . d == 0_No & 0_No = uInt . 0 & uInt . 0 = uDyadic . 0 ) by A33, SURREALO:4, Def1, Def5;
then ( 0 <= d & d <= 0 ) by Th24;
hence contradiction by A6; :: thesis: verum

end;

then consider x3, y3, p3 being Nat such that
A65: ( Z1 == uDyadic . (x3 + (y3 / (2 |^ p3))) & y3 < 2 |^ p3 & x3 + p3 < k + (p + 1) ) by Th25, A60, A62;
A66: ( L_ (uDyadic . d) << {(uDyadic . d)} & {(uDyadic . d)} << R_ (uDyadic . d) ) by SURREALO:11;
A67: uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) == Z1

proof

assume not uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) == Z1 ; :: thesis: contradiction

per cases then ( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) < Z1 or Z1 < uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) ) ;

suppose uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) < Z1 ; :: thesis: contradiction

then A68: ( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) < uDyadic . (x3 + (y3 / (2 |^ p3))) & uDyadic . (x3 + (y3 / (2 |^ p3))) < uDyadic . d ) by A59, A65, SURREALO:4, SURREALO:21;
then ( k + (m / (2 |^ p)) < x3 + (y3 / (2 |^ p3)) & x3 + (y3 / (2 |^ p3)) < k + (((2 * m) + 1) / (2 |^ (p + 1))) ) by Th24, A10, A16;
then ( k <= x3 & x3 <= k ) by Th33, A65, A15, A10;
then A69: k = x3 by XXREAL_0:1;
then p3 < p + 1 by A65, XREAL_1:6;
then p3 <= p by NAT_1:13;
then reconsider P = p - p3 as Nat by NAT_1:21;
p = p3 + P ;
then 2 |^ p = (2 |^ p3) * (2 |^ P) by NEWTON:8;
then 2 |^ (p + 1) = (2 |^ p3) * (2 * (2 |^ P)) by A11;
then A70: y3 / (2 |^ p3) = (y3 * (2 * (2 |^ P))) / (2 |^ (p + 1)) by XCMPLX_1:91;
A71: m / (2 |^ p) = (2 * m) / (2 |^ (p + 1)) by A11, XCMPLX_1:91;
( (2 * m) / (2 |^ (p + 1)) < (y3 * (2 * (2 |^ P))) / (2 |^ (p + 1)) & (y3 * (2 * (2 |^ P))) / (2 |^ (p + 1)) < ((2 * m) + 1) / (2 |^ (p + 1)) ) by A70, A71, A68, A69, XREAL_1:6, Th24, A10, A16;
then ( 2 * m < y3 * (2 * (2 |^ P)) & y3 * (2 * (2 |^ P)) < (2 * m) + 1 ) by XREAL_1:72;
hence contradiction by NAT_1:13; :: thesis: verum

end;

suppose A72: Z1 < uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) ; :: thesis: contradiction

uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) <= uDyadic . d by A66, SURREALO:21, A12;
then uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) < Z2 by A59, SURREALO:21, SURREALO:4;
then ( L_ z << {(uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)))} & {(uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)))} << R_ z ) by A72, A55, A56, SURREALO:21;
then born z c= born (uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p))) by SURREALO:51, A61;
hence contradiction by A26, A61, A28, ORDINAL1:12; :: thesis: verum

end;

end;

end;

A73: uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) == Z2

proof

assume A74: not uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) == Z2 ; :: thesis: contradiction
A75: 0_No <= Z2 by A63, A56, SURREALO:21;
not Z2 == uDyadic . (k + (p + 1))

proof

assume A76: Z2 == uDyadic . (k + (p + 1)) ; :: thesis: contradiction
A77: k + p < (k + p) + 1 by NAT_1:13;
A78: p = 0

proof

assume p <> 0 ; :: thesis: contradiction
then ( ((2 * m) + 1) / (2 |^ (p + 1)) < 1 & 1 <= p ) by NAT_1:14, A10, XREAL_1:189;
then ((2 * m) + 1) / (2 |^ (p + 1)) < p by XXREAL_0:2;
then uDyadic . d <= uDyadic . (k + p) by Th24, A10, XREAL_1:6;
then ( Z1 < uDyadic . (k + p) & uDyadic . (k + p) < Z2 ) by A76, A77, SURREALO:4, SURREALO:21, A59, Th24;
then ( {Z1} << {(uDyadic . (k + p))} & {(uDyadic . (k + p))} << {Z2} ) by SURREALO:21;
then A79: ( born z c= born (uDyadic . (k + p)) & born (uDyadic . (k + p)) = born (uInt . (k + p)) & born (uInt . (k + p)) = k + p ) by Def5, A61, A55, A56, SURREALO:51, Th4;
Segm ((k + (p + 1)) + 1) c= Segm (k + p) by A61, A19, A14, A79, SURREALO:def 5;
then ( (k + p) + 2 = (k + (p + 1)) + 1 & (k + (p + 1)) + 1 <= (k + p) + 0 ) by NAT_1:39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

then (2 * m) + 1 < 1 + 1 by A10;
then A80: m = 0 by NAT_1:14, XREAL_1:6;
2 |^ p = 1 by A78, NEWTON:4;
hence contradiction by A80, A76, A78, A74; :: thesis: verum

end;

then consider x4, y4, p4 being Nat such that
A81: ( Z2 == uDyadic . (x4 + (y4 / (2 |^ p4))) & y4 < 2 |^ p4 & x4 + p4 < k + (p + 1) ) by Th25, A60, A75;

per cases ( Z2 < uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) or uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) < Z2 ) by A74;

suppose Z2 < uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) ; :: thesis: contradiction

then ( uDyadic . d < uDyadic . (x4 + (y4 / (2 |^ p4))) & uDyadic . (x4 + (y4 / (2 |^ p4))) < uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) ) by A59, SURREALO:21, A81, SURREALO:4;
then A82: ( k + (((2 * m) + 1) / (2 |^ (p + 1))) < x4 + (y4 / (2 |^ p4)) & x4 + (y4 / (2 |^ p4)) < k + ((m + 1) / (2 |^ p)) ) by Th24, A10, A17;
then k <= x4 by A10, A81, Th33;
then k + (p + 1) <= x4 + (p + 1) by XREAL_1:6;
then x4 + p4 < x4 + (p + 1) by A81, XXREAL_0:2;
then reconsider P = (p + 1) - p4 as Nat by NAT_1:21, XREAL_1:6;
p + 1 = p4 + P ;
then 2 |^ (p + 1) = (2 |^ p4) * (2 |^ P) by NEWTON:8;
then A83: y4 / (2 |^ p4) = (y4 * (2 |^ P)) / (2 |^ (p + 1)) by XCMPLX_1:91;
A84: ( k + (((2 * m) + 1) / (2 |^ (p + 1))) = ((k * (2 |^ (p + 1))) + ((2 * m) + 1)) / (2 |^ (p + 1)) & x4 + ((y4 * (2 |^ P)) / (2 |^ (p + 1))) = ((x4 * (2 |^ (p + 1))) + (y4 * (2 |^ P))) / (2 |^ (p + 1)) & k + ((2 * (m + 1)) / (2 |^ (p + 1))) = ((k * (2 |^ (p + 1))) + (2 * (m + 1))) / (2 |^ (p + 1)) ) by XCMPLX_1:113;
( ((k * (2 |^ (p + 1))) + ((2 * m) + 1)) / (2 |^ (p + 1)) < ((x4 * (2 |^ (p + 1))) + (y4 * (2 |^ P))) / (2 |^ (p + 1)) & ((x4 * (2 |^ (p + 1))) + (y4 * (2 |^ P))) / (2 |^ (p + 1)) < ((k * (2 |^ (p + 1))) + (2 * (m + 1))) / (2 |^ (p + 1)) ) by A82, A83, A84, A11, XCMPLX_1:91;
then ( (k * (2 |^ (p + 1))) + ((2 * m) + 1) < (x4 * (2 |^ (p + 1))) + (y4 * (2 |^ P)) & (x4 * (2 |^ (p + 1))) + (y4 * (2 |^ P)) < (k * (2 |^ (p + 1))) + (2 * (m + 1)) ) by XREAL_1:72;
then ((k * (2 |^ (p + 1))) + ((2 * m) + 1)) + 1 < (k * (2 |^ (p + 1))) + (2 * (m + 1)) by NAT_1:13;
hence contradiction ; :: thesis: verum

end;

suppose A85: uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) < Z2 ; :: thesis: contradiction

uDyadic . d <= uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) by A66, SURREALO:21, A12;
then Z1 < uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) by A59, SURREALO:21, SURREALO:4;
then ( L_ z << {(uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)))} & {(uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)))} << R_ z ) by A85, A55, A56, SURREALO:21;
then born z c= born (uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p))) by SURREALO:51, A61;
hence contradiction by A26, A61, A28, ORDINAL1:12; :: thesis: verum

end;

end;

end;

( uDyadic . (((k * (2 |^ p)) + m) / (2 |^ p)) = Z1 & uDyadic . ((((k * (2 |^ p)) + m) + 1) / (2 |^ p)) = Z2 ) by A67, A73, A29, SURREALO:50;
hence contradiction by A30, A12, A55, A56; :: thesis: verum

end;

end;

end;

hence ( ( for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . d in born_eq_set (uDyadic . d) & (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered ) by A29, A12, A27, SURREALO:def 6; :: thesis: verum

end;

let d be Dyadic; :: thesis: ( uDyadic . d in Day (n + 1) implies uDyadic . d is uniq-surreal )
set D = uDyadic . d;
assume A86: uDyadic . d in Day (n + 1) ; :: thesis: uDyadic . d is uniq-surreal

per cases ( uDyadic . d in Day n or not uDyadic . d in Day n ) ;

suppose uDyadic . d in Day n ; :: thesis: uDyadic . d is uniq-surreal

hence uDyadic . d is uniq-surreal by A3; :: thesis: verum

end;

suppose A87: not uDyadic . d in Day n ; :: thesis: uDyadic . d is uniq-surreal

not born (uDyadic . d) c= n

proof

assume born (uDyadic . d) c= n ; :: thesis: contradiction
then ( uDyadic . d in Day (born (uDyadic . d)) & Day (born (uDyadic . d)) c= Day n ) by SURREAL0:def 18, SURREAL0:35;
hence contradiction by A87; :: thesis: verum

end;

then A88: ( Segm (n + 1) = succ (Segm n) & succ (Segm n) c= born (uDyadic . d) & born (uDyadic . d) c= n + 1 ) by A86, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18, NAT_1:38;
then A89: born (uDyadic . d) = n + 1 by XBOOLE_0:def 10;

per cases ( d is Integer or ( 0 <= d & d is not Integer ) or ( not 0 <= d & d is not Integer ) ) ;

suppose d is Integer ; :: thesis: uDyadic . d is uniq-surreal

then reconsider i = d as Integer ;
uDyadic . d = uInt . i by Def5;
hence uDyadic . d is uniq-surreal ; :: thesis: verum

end;

suppose A90: ( 0 <= d & d is not Integer ) ; :: thesis: uDyadic . d is uniq-surreal

uDyadic . d in (Day (n + 1)) \ (Day n) by A87, A86, XBOOLE_0:def 5;
then ( ( for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . d in born_eq_set (uDyadic . d) & (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered ) by A90, A5;
hence uDyadic . d is uniq-surreal by SURREALO:49; :: thesis: verum

end;

suppose A91: ( not 0 <= d & d is not Integer ) ; :: thesis: uDyadic . d is uniq-surreal

- (- d) = d ;
then A92: - d is not Integer by A91;
set E = uDyadic . (- d);
A93: uDyadic . (- d) = - (uDyadic . d) by Th27;
A94: uDyadic . (- d) in Day (n + 1) by A93, SURREALR:11, A86;
A95: - (uDyadic . (- d)) = uDyadic . d by A93;
then not uDyadic . (- d) in Day n by SURREALR:11, A87;
then uDyadic . (- d) in (Day (n + 1)) \ (Day n) by A94, XBOOLE_0:def 5;
then A96: ( ( for z being Surreal st z in born_eq_set (uDyadic . (- d)) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . (- d) <> z holds
(card (L_ (uDyadic . (- d)))) (+) (card (R_ (uDyadic . (- d)))) in (card (L_ z)) (+) (card (R_ z)) ) & uDyadic . (- d) in born_eq_set (uDyadic . (- d)) & (L_ (uDyadic . (- d))) \/ (R_ (uDyadic . (- d))) is uniq-surreal-membered ) by A92, A91, A5;
A97: for z being Surreal st z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z holds
(card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z implies (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) )
assume A98: ( z in born_eq_set (uDyadic . d) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uDyadic . d <> z ) ; :: thesis: (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z))
set Z = - z;
A99: ( L_ (- (uDyadic . d)) = -- (R_ (uDyadic . d)) & R_ (- (uDyadic . d)) = -- (L_ (uDyadic . d)) ) by SURREALR:8;
A100: ( L_ (- z) = -- (R_ z) & R_ (- z) = -- (L_ z) ) by SURREALR:8;
A101: - z <> uDyadic . (- d) by A98, A95;
A102: (L_ (- z)) \/ (R_ (- z)) is uniq-surreal-membered

proof

let o be object ; :: according to SURREALO:def 12 :: thesis: ( not o in (L_ (- z)) \/ (R_ (- z)) or o is set )
assume o in (L_ (- z)) \/ (R_ (- z)) ; :: thesis: o is set
then o in -- ((L_ z) \/ (R_ z)) by A100, SURREALR:20;
then consider x being Surreal such that
A103: ( x in (L_ z) \/ (R_ z) & o = - x ) by SURREALR:def 4;
A104: x is uSurreal by A98, A103;
A105: Segm (n + 1) = succ (Segm n) by NAT_1:38;
( born z = born_eq z & born_eq z = born_eq (uDyadic . d) & born_eq (uDyadic . d) c= born (uDyadic . d) ) by A98, SURREALO:35, SURREALO:def 5;
then ( born x in born z & born z c= n + 1 ) by A103, A88, SURREALO:1, XBOOLE_0:def 10;
then ( x in Day (born x) & Day (born x) c= Day n ) by SURREAL0:def 18, SURREAL0:35, A105, ORDINAL1:22;
hence o is set by A103, A104, A3; :: thesis: verum

end;

A106: ( card (L_ (- z)) = card (R_ z) & card (R_ (- z)) = card (L_ z) ) by A100, SURREALR:17;
( card (L_ (uDyadic . (- d))) = card (R_ (uDyadic . d)) & card (R_ (uDyadic . (- d))) = card (L_ (uDyadic . d)) ) by A99, A93, SURREALR:17;
hence (card (L_ (uDyadic . d))) (+) (card (R_ (uDyadic . d))) in (card (L_ z)) (+) (card (R_ z)) by A102, A106, A96, A101, A98, A93, SURREALR:14; :: thesis: verum

end;

(L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) is uniq-surreal-membered

proof

A107: ( L_ (uDyadic . d) = -- (R_ (uDyadic . (- d))) & R_ (uDyadic . d) = -- (L_ (uDyadic . (- d))) ) by A95, SURREALR:8;
let o be object ; :: according to SURREALO:def 12 :: thesis: ( not o in (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) or o is set )
assume o in (L_ (uDyadic . d)) \/ (R_ (uDyadic . d)) ; :: thesis: o is set
then o in -- ((L_ (uDyadic . (- d))) \/ (R_ (uDyadic . (- d)))) by A107, SURREALR:20;
then consider x being Surreal such that
A108: ( x in (L_ (uDyadic . (- d))) \/ (R_ (uDyadic . (- d))) & o = - x ) by SURREALR:def 4;
A109: x is uSurreal by A96, A108;
A110: Segm (n + 1) = succ (Segm n) by NAT_1:38;
born (uDyadic . (- d)) = born (uDyadic . d) by A93, SURREALR:12;
then born x c= Segm n by A108, A89, SURREALO:1, A110, ORDINAL1:22;
then ( x in Day (born x) & Day (born x) c= Day n ) by SURREAL0:def 18, SURREAL0:35;
hence o is set by A108, A109, A3; :: thesis: verum

end;

hence uDyadic . d is uniq-surreal by SURREALO:49, A97, Th30; :: thesis: verum

end;

end;

end;

end;

end;

let x be Surreal; :: thesis: ( x in Day (n + 1) & x is uniq-surreal implies - x is uniq-surreal )
assume A111: ( x in Day (n + 1) & x is uniq-surreal ) ; :: thesis: - x is uniq-surreal
consider d being Dyadic such that
A112: ( x == uDyadic . d & uDyadic . d in Day (n + 1) ) by A111, Th35;
A113: uDyadic . (- d) = - (uDyadic . d) by Th27;
then A114: uDyadic . (- d) is uniq-surreal by A4, A112, SURREALR:11;
uDyadic . d is uniq-surreal by A112, A4;
hence - x is uniq-surreal by A113, A114, A112, A111, SURREALO:41; :: thesis: verum

end;

A115: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
ex n being Nat st uDyadic . d in Day n by Th36;
hence uDyadic . d is uniq-surreal by A115; :: thesis: verum