let x be Surreal; :: thesis: ( born x is finite & (card (L_ x)) (+) (card (R_ x)) c= 1 implies ex i being Integer st x == uInt . i )
assume A1: ( born x is finite & (card (L_ x)) (+) (card (R_ x)) c= 1 ) ; :: thesis: ex i being Integer st x == uInt . i
A2: born x = born (- x) by SURREALR:12;

per cases ( (card (L_ x)) (+) (card (R_ x)) = 1 or (card (L_ x)) (+) (card (R_ x)) <> 1 ) ;

suppose (card (L_ x)) (+) (card (R_ x)) = 1 ; :: thesis: ex i being Integer st x == uInt . i

then consider y being Surreal such that
A3: ( x = [{},{y}] or x = [{y},{}] ) by SURREALO:47;

per cases ( x = [{},{y}] or x = [{y},{}] ) by A3;

suppose x = [{},{y}] ; :: thesis: ex i being Integer st x == uInt . i

then ( -- (R_ x) = -- {y} & -- {y} = {(- y)} & -- (L_ x) = -- {} & -- {} = {} ) by SURREALR:21, SURREALR:22;
then A4: - x = [{(- y)},{}] by SURREALR:7;

per cases ( - y < 0_No or 0_No <= - y ) ;

suppose - y < 0_No ; :: thesis: ex i being Integer st x == uInt . i

then - x == 0_No by A4, Th16;
then ( x = - (- x) & - (- x) == 0_No & 0_No = uInt . 0 ) by Def1, SURREALR:23, SURREALR:10;
hence ex i being Integer st x == uInt . i ; :: thesis: verum

end;

suppose 0_No <= - y ; :: thesis: ex i being Integer st x == uInt . i

then consider n being Nat such that
A5: ( - x == uInt . (n + 1) & uInt . n <= - y & - y < uInt . (n + 1) & n in born x ) by A4, A1, A2, Th17;
( x = - (- x) & - (- x) == - (uInt . (n + 1)) & - (uInt . (n + 1)) = uInt . (- (n + 1)) ) by A5, SURREALR:10, Th12;
hence ex i being Integer st x == uInt . i ; :: thesis: verum

end;

end;

end;

suppose A6: x = [{y},{}] ; :: thesis: ex i being Integer st x == uInt . i

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

suppose y < 0_No ; :: thesis: ex i being Integer st x == uInt . i

then ( x == 0_No & 0_No = uInt . 0 ) by Def1, A6, Th16;
hence ex i being Integer st x == uInt . i ; :: thesis: verum

end;

suppose 0_No <= y ; :: thesis: ex i being Integer st x == uInt . i

then ex n being Nat st
( x == uInt . (n + 1) & uInt . n <= y & y < uInt . (n + 1) & n in born x ) by A6, A1, Th17;
hence ex i being Integer st x == uInt . i ; :: thesis: verum

end;

end;

end;

end;

end;

suppose (card (L_ x)) (+) (card (R_ x)) <> 1 ; :: thesis: ex i being Integer st x == uInt . i

then ( (card (L_ x)) (+) (card (R_ x)) in 1 & 1 = succ 0 ) by A1, XBOOLE_0:def 8, ORDINAL1:11;
then (card (L_ x)) (+) (card (R_ x)) = 0 ;
then x = 0_No by SURREALO:46;
then x = uInt . 0 by Def1;
hence ex i being Integer st x == uInt . i ; :: thesis: verum

end;

end;