let r be Real; :: thesis: for z being Surreal st z > 0_No holds
[ { ((uReal . (r - e1)) * z) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * z) where e2 is positive Real : verum } ] is Surreal
let a be Surreal; :: thesis: ( a > 0_No implies [ { ((uReal . (r - e1)) * a) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * a) where e2 is positive Real : verum } ] is Surreal )
assume A1: a > 0_No ; :: thesis: [ { ((uReal . (r - e1)) * a) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * a) where e2 is positive Real : verum } ] is Surreal
set Sl = { ((uReal . (r - e)) * a) where e is positive Real : verum } ;
set Sr = { ((uReal . (r + e)) * a) where e is positive Real : verum } ;

now :: thesis: for o being object st o in { ((uReal . (r - e)) * a) where e is positive Real : verum } holds
o is surreal

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

end;

then reconsider Sl = { ((uReal . (r - e)) * a) where e is positive Real : verum } as surreal-membered set by SURREAL0:def 16;

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

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

end;

then reconsider Sr = { ((uReal . (r + e)) * a) where e is positive Real : verum } as surreal-membered set by SURREAL0:def 16;
consider M being Ordinal such that
A2: 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;
Sl << Sr

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in Sl or not y in Sr or not y <= x )
assume A3: ( x in Sl & y in Sr ) ; :: thesis: not y <= x
consider e1 being positive Real such that
A4: x = (uReal . (r - e1)) * a by A3;
consider e2 being positive Real such that
A5: y = (uReal . (r + e2)) * a by A3;
A6: 0_No + x == (0_No + ((uReal . r) * a)) - ((uReal . e1) * a) by Th30, A4;
A7: 0_No + y == (0_No + ((uReal . r) * a)) + ((uReal . e2) * a) by Th30, A5;
( - (uReal . e1) == uReal . (- e1) & uReal . (- e1) < uReal . e2 ) by SURREALN:56, SURREALN:51;
then - (uReal . e1) < uReal . e2 by SURREALO:9;
then a * (- (uReal . e1)) < a * (uReal . e2) by A1, SURREALR:70;
then - (a * (uReal . e1)) < a * (uReal . e2) by SURREALR:58;
then ((uReal . r) * a) + (- (a * (uReal . e1))) < ((uReal . r) * a) + (a * (uReal . e2)) by SURREALR:44;
then ((uReal . r) * a) + (- (a * (uReal . e1))) < y by A7, SURREALO:9;
hence x < y by A6, SURREALO:9; :: thesis: verum

end;

then [Sl,Sr] in Day M by A2, SURREAL0:46;
hence [ { ((uReal . (r - e1)) * a) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * a) where e2 is positive Real : verum } ] is Surreal ; :: thesis: verum