i in INT by INT_1:def 2;
then consider o being Nat such that
A1: ( i = o or i = - o ) by INT_1:def 1;

per cases ( i = o or i = - o ) by A1;

suppose A2: i = o ; :: thesis: uInt . i is uniq-surreal

defpred S₁[ Nat] means uInt . i is uniq-surreal ;
A3: S₁[ 0 ] by Def1;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider sn = uInt . n as uSurreal ;
set n1 = n + 1;
set x = uInt . (n + 1);
A5: uInt . (n + 1) in Day (born (uInt . (n + 1))) by SURREAL0:def 18;
A6: ( born_eq (uInt . (n + 1)) = n + 1 & n + 1 = born (uInt . (n + 1)) ) by Th5, Th4;
then A7: uInt . (n + 1) in born_eq_set (uInt . (n + 1)) by A5, SURREALO:def 6;
A8: uInt . (n + 1) = [{sn},{}] by Def1;
then A9: (L_ (uInt . (n + 1))) \/ (R_ (uInt . (n + 1))) is uniq-surreal-membered ;
for z being Surreal st z in born_eq_set (uInt . (n + 1)) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uInt . (n + 1) <> z holds
(card (L_ (uInt . (n + 1)))) (+) (card (R_ (uInt . (n + 1)))) in (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in born_eq_set (uInt . (n + 1)) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uInt . (n + 1) <> z implies (card (L_ (uInt . (n + 1)))) (+) (card (R_ (uInt . (n + 1)))) in (card (L_ z)) (+) (card (R_ z)) )
assume that
A10: ( z in born_eq_set (uInt . (n + 1)) & (L_ z) \/ (R_ z) is uniq-surreal-membered ) and
A11: uInt . (n + 1) <> z and
A12: not (card (L_ (uInt . (n + 1)))) (+) (card (R_ (uInt . (n + 1)))) in (card (L_ z)) (+) (card (R_ z)) ; :: thesis: contradiction
A13: z == uInt . (n + 1) by A10, SURREALO:def 6;
A14: (card (L_ (uInt . (n + 1)))) (+) (card (R_ (uInt . (n + 1)))) = 1 by A8, SURREALO:47;
then (card (L_ z)) (+) (card (R_ z)) c= 1 by A12, ORDINAL1:16;
then reconsider cz = (card (L_ z)) (+) (card (R_ z)) as Nat ;
cz <> 0

proof

assume cz = 0 ; :: thesis: contradiction
then A15: z = 0_No by SURREALO:46;
uInt . 0 < uInt . (n + 1) by Th3;
hence contradiction by A13, A15, Def1; :: thesis: verum

end;

then A16: 1 <= cz by NAT_1:14;
Segm cz c= Segm 1 by A14, A12, ORDINAL1:16;
then cz <= 1 by NAT_1:39;
then consider r being Surreal such that
A17: ( z = [{},{r}] or z = [{r},{}] ) by SURREALO:47, A16, XXREAL_0:1;
A18: r in (L_ z) \/ (R_ z) by A17, TARSKI:def 1;
then reconsider r = r as uSurreal by A10;
A19: ( born z = born_eq z & born_eq z = born_eq (uInt . (n + 1)) ) by A10, SURREALO:35;
A20: born r in n + 1 by A19, A6, SURREALO:1, A18;
then A21: ( r in Day (born r) & Day (born r) c= Day (n + 1) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;

per cases ( z = [{},{r}] or z = [{r},{}] ) by A17;

suppose A22: z = [{},{r}] ; :: thesis: contradiction

A23: ( L_ (uInt . (n + 1)) << {z} & {(uInt . (n + 1))} << R_ z & L_ z << {(uInt . (n + 1))} ) by A13, SURREAL0:43;
( uInt . (n + 1) in {(uInt . (n + 1))} & r in {r} ) by TARSKI:def 1;
hence contradiction by A21, Th2, A23, A22; :: thesis: verum

end;

suppose A24: z = [{r},{}] ; :: thesis: contradiction

then A25: not r == sn by A11, A8, SURREALO:50;
n + 1 = Segm (n + 1) ;
then born r in succ (Segm n) by A20, NAT_1:38;
then A26: ( r in Day (born r) & Day (born r) c= Day n ) by ORDINAL1:22, SURREAL0:35, SURREAL0:def 18;
( L_ z << {sn} & {z} << R_ sn ) by Th7, A24, SURREALO:21, A26, Th2, A25;
then not L_ (uInt . (n + 1)) << {z} by SURREAL0:43, A8, SURREALO:21;
hence contradiction by A13, SURREAL0:43; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] by A7, A9, SURREALO:49; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence uInt . i is uniq-surreal by A2; :: thesis: verum

end;

suppose A27: i = - o ; :: thesis: uInt . i is uniq-surreal

defpred S₁[ Nat] means uInt . (- i) is uniq-surreal ;
A28: S₁[ 0 ] by Def1;
A29: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then reconsider sn = uInt . (- n) as uSurreal ;
set n1 = n + 1;
set x = uInt . (- (n + 1));
A30: uInt . (- (n + 1)) in Day (born (uInt . (- (n + 1)))) by SURREAL0:def 18;
A31: ( born_eq (uInt . (- (n + 1))) = n + 1 & n + 1 = born (uInt . (- (n + 1))) ) by Th5, Th4;
then A32: uInt . (- (n + 1)) in born_eq_set (uInt . (- (n + 1))) by A30, SURREALO:def 6;
A33: uInt . (- (n + 1)) = [{},{sn}] by Def1;
then A34: (L_ (uInt . (- (n + 1)))) \/ (R_ (uInt . (- (n + 1)))) is uniq-surreal-membered ;
for z being Surreal st z in born_eq_set (uInt . (- (n + 1))) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uInt . (- (n + 1)) <> z holds
(card (L_ (uInt . (- (n + 1))))) (+) (card (R_ (uInt . (- (n + 1))))) in (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis: ( z in born_eq_set (uInt . (- (n + 1))) & (L_ z) \/ (R_ z) is uniq-surreal-membered & uInt . (- (n + 1)) <> z implies (card (L_ (uInt . (- (n + 1))))) (+) (card (R_ (uInt . (- (n + 1))))) in (card (L_ z)) (+) (card (R_ z)) )
assume that
A35: ( z in born_eq_set (uInt . (- (n + 1))) & (L_ z) \/ (R_ z) is uniq-surreal-membered ) and
A36: uInt . (- (n + 1)) <> z and
A37: not (card (L_ (uInt . (- (n + 1))))) (+) (card (R_ (uInt . (- (n + 1))))) in (card (L_ z)) (+) (card (R_ z)) ; :: thesis: contradiction
A38: z == uInt . (- (n + 1)) by A35, SURREALO:def 6;
A39: (card (L_ (uInt . (- (n + 1))))) (+) (card (R_ (uInt . (- (n + 1))))) = 1 by A33, SURREALO:47;
then (card (L_ z)) (+) (card (R_ z)) c= 1 by A37, ORDINAL1:16;
then reconsider cz = (card (L_ z)) (+) (card (R_ z)) as Nat ;
cz <> 0

proof

assume cz = 0 ; :: thesis: contradiction
then A40: z = 0_No by SURREALO:46;
uInt . (- (n + 1)) < uInt . 0 by Th3;
hence contradiction by A38, A40, Def1; :: thesis: verum

end;

then A41: 1 <= cz by NAT_1:14;
Segm cz c= Segm 1 by A39, A37, ORDINAL1:16;
then cz <= 1 by NAT_1:39;
then consider r being Surreal such that
A42: ( z = [{},{r}] or z = [{r},{}] ) by SURREALO:47, A41, XXREAL_0:1;
A43: r in (L_ z) \/ (R_ z) by A42, TARSKI:def 1;
then reconsider r = r as uSurreal by A35;
A44: ( born z = born_eq z & born_eq z = born_eq (uInt . (- (n + 1))) ) by A35, SURREALO:35;
A45: born r in n + 1 by A44, A31, SURREALO:1, A43;
then A46: ( r in Day (born r) & Day (born r) c= Day (n + 1) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;

per cases ( z = [{r},{}] or z = [{},{r}] ) by A42;

suppose A47: z = [{r},{}] ; :: thesis: contradiction

A48: ( L_ (uInt . (- (n + 1))) << {z} & {(uInt . (- (n + 1)))} << R_ z & L_ z << {(uInt . (- (n + 1)))} ) by A38, SURREAL0:43;
( uInt . (- (n + 1)) in {(uInt . (- (n + 1)))} & r in {r} ) by TARSKI:def 1;
hence contradiction by A46, A47, A48, Th2; :: thesis: verum

end;

suppose A49: z = [{},{r}] ; :: thesis: contradiction

then A50: not r == sn by A36, A33, SURREALO:50;
n + 1 = Segm (n + 1) ;
then born r in succ (Segm n) by A45, NAT_1:38;
then A51: ( r in Day (born r) & Day (born r) c= Day n ) by ORDINAL1:22, SURREAL0:35, SURREAL0:def 18;
( R_ z >> {sn} & {z} >> L_ sn ) by Th7, A49, A51, Th2, A50, SURREALO:21;
then not R_ (uInt . (- (n + 1))) >> {z} by SURREAL0:43, A33, SURREALO:21;
hence contradiction by A38, SURREAL0:43; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] by A32, A34, SURREALO:49; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A28, A29);
hence uInt . i is uniq-surreal by A27; :: thesis: verum

end;

end;