let i be Integer; :: thesis: for x being Surreal holds
( [{(uInt . (i - 1))},{(uInt . (i + 1))}] is Surreal & ( x = [{(uInt . (i - 1))},{(uInt . (i + 1))}] implies x == uInt . i ) )
let x be Surreal; :: thesis: ( [{(uInt . (i - 1))},{(uInt . (i + 1))}] is Surreal & ( x = [{(uInt . (i - 1))},{(uInt . (i + 1))}] implies x == uInt . i ) )
set S = uInt . i;
i + (- 1) < i + 1 by XREAL_1:6;
hence [{(uInt . (i - 1))},{(uInt . (i + 1))}] is Surreal by Th9, SURREALO:22; :: thesis: ( x = [{(uInt . (i - 1))},{(uInt . (i + 1))}] implies x == uInt . i )
assume A1: x = [{(uInt . (i - 1))},{(uInt . (i + 1))}] ; :: thesis: x == uInt . i
uInt . (i - 1) < uInt . i by XREAL_1:44, Th9;
then A2: L_ x << {(uInt . i)} by A1, SURREALO:21;
A3: ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) )

proof

per cases ( i = 0 or i > 0 or 0 > i ) ;

suppose i = 0 ; :: thesis: ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) )

then uInt . i = 0_No by Def1;
hence ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) ) ; :: thesis: verum

end;

suppose A4: i > 0 ; :: thesis: ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) )

then reconsider I = i as Element of NAT by INT_1:3;
reconsider i1 = I - 1 as Nat by NAT_1:20, A4;
i = i1 + 1 ;
then A5: uInt . i = [{(uInt . i1)},{}] by Def1;
uInt . i1 <= uInt . (i - 1) ;
then not L_ x << {(uInt . i1)} by A1, SURREALO:21;
then uInt . i1 < x by SURREAL0:43;
hence ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) ) by SURREALO:21, A5; :: thesis: verum

end;

suppose A6: 0 > i ; :: thesis: ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) )

then reconsider I = - i as Element of NAT by INT_1:3;
reconsider i1 = I - 1 as Nat by NAT_1:20, A6;
i = - (i1 + 1) ;
then A7: uInt . i = [{},{(uInt . (- i1))}] by Def1;
( not L_ (uInt . (- i1)) << {x} or not {(uInt . (- i1))} << R_ x ) by SURREALO:3, SURREALO:21, A1;
then not uInt . (- i1) <= x by SURREAL0:43;
hence ( L_ (uInt . i) << {x} & {x} << R_ (uInt . i) ) by SURREALO:21, A7; :: thesis: verum

end;

end;

end;

uInt . i < uInt . (i + 1) by Th9, XREAL_1:29;
then {(uInt . i)} << R_ x by A1, SURREALO:21;
hence x == uInt . i by A2, A3, SURREAL0:43; :: thesis: verum