set L = { (x - ((uInt . n) ")) where n is positive Nat : verum } ;
set R = { (x + ((uInt . n) ")) where n is positive Nat : verum } ;
A1: { (x - ((uInt . n) ")) where n is positive Nat : verum } is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in { (x - ((uInt . n) ")) where n is positive Nat : verum } or o is surreal )
assume o in { (x - ((uInt . n) ")) where n is positive Nat : verum } ; :: thesis: o is surreal
then ex n being positive Nat st o = x - ((uInt . n) ") ;
hence o is surreal ; :: thesis: verum

end;

{ (x + ((uInt . n) ")) where n is positive Nat : verum } is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in { (x + ((uInt . n) ")) where n is positive Nat : verum } or o is surreal )
assume o in { (x + ((uInt . n) ")) where n is positive Nat : verum } ; :: thesis: o is surreal
then ex n being positive Nat st o = x + ((uInt . n) ") ;
hence o is surreal ; :: thesis: verum

end;

then reconsider L = { (x - ((uInt . n) ")) where n is positive Nat : verum } , R = { (x + ((uInt . n) ")) where n is positive Nat : verum } as surreal-membered set by A1;
consider M being Ordinal such that
A2: for o being object st o in L \/ R holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
L << R

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in L or not r in R or not r <= l )
assume A3: ( l in L & r in R ) ; :: thesis: not r <= l
consider nL being positive Nat such that
A4: l = x - ((uInt . nL) ") by A3;
consider nR being positive Nat such that
A5: r = x + ((uInt . nR) ") by A3;
( - ((uInt . nL) ") < - 0_No & - 0_No = 0_No ) by SURREALR:10, SURREALI:def 8;
then A6: ( x + (- ((uInt . nL) ")) < x + 0_No & x + 0_No = x ) by SURREALR:44;
( x = x + 0_No & x + 0_No <= x + ((uInt . nR) ") ) by SURREALR:44, SURREALI:def 8;
hence not r <= l by A4, A5, A6, SURREALO:4; :: thesis: verum

end;

then [L,R] in Day M by A2, SURREAL0:46;
then reconsider LR = [L,R] as Surreal ;
take LR ; :: thesis: ( L_ LR = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ LR = { (x + ((uInt . n) ")) where n is positive Nat : verum } )
thus ( L_ LR = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ LR = { (x + ((uInt . n) ")) where n is positive Nat : verum } ) ; :: thesis: verum