let r be Real; :: thesis: [ { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] is Surreal
set Sl = { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } ;
set Sr = { (uReal . (r + e2)) where e2 is positive Real : verum } ;

now :: thesis: for o being object st o in { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } holds
o is surreal

let o be object ; :: thesis: ( o in { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } implies o is surreal )
assume o in { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } ; :: thesis: o is surreal
then ex e1 being positive Real st
( o = uReal . (r - e1) & r - e1 > 0 ) ;
hence o is surreal ; :: thesis: verum

end;

then reconsider SL = { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } as surreal-membered set by SURREAL0:def 16;

now :: thesis: for o being object st o in { (uReal . (r + e2)) where e2 is positive Real : verum } holds
o is surreal

let o be object ; :: thesis: ( o in { (uReal . (r + e2)) where e2 is positive Real : verum } implies o is surreal )
assume o in { (uReal . (r + e2)) where e2 is positive Real : verum } ; :: thesis: o is surreal
then ex e2 being positive Real st o = uReal . (r + e2) ;
hence o is surreal ; :: thesis: verum

end;

then reconsider SR = { (uReal . (r + e2)) where e2 is positive Real : verum } as surreal-membered set by SURREAL0:def 16;
consider M being Ordinal such that
A1: for o being object st o in SL \/ SR holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
{ (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } << { (uReal . (r + e2)) where e2 is positive Real : verum }

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } or not y in { (uReal . (r + e2)) where e2 is positive Real : verum } or not y <= x )
assume A2: ( x in { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } & y in { (uReal . (r + e2)) where e2 is positive Real : verum } ) ; :: thesis: not y <= x
consider e1 being positive Real such that
A3: ( x = uReal . (r - e1) & r - e1 > 0 ) by A2;
consider e2 being positive Real such that
A4: y = uReal . (r + e2) by A2;
( r - e1 < r & r < r + e2 ) by XREAL_1:29, XREAL_1:44;
then r - e1 < r + e2 by XXREAL_0:2;
hence not y <= x by A3, A4, SURREALN:51; :: thesis: verum

end;

then [SL,SR] in Day M by A1, SURREAL0:46;
hence [ { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] is Surreal ; :: thesis: verum