let r be Real; :: thesis: for z, x being Surreal st x = [ { ((uReal . (r - e1)) * (No_omega^ z)) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * (No_omega^ z)) where e2 is positive Real : verum } ] holds
(uReal . r) * (No_omega^ z) == x
let a, X be Surreal; :: thesis: ( X = [ { ((uReal . (r - e1)) * (No_omega^ a)) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * (No_omega^ a)) where e2 is positive Real : verum } ] implies (uReal . r) * (No_omega^ a) == X )
assume A1: X = [ { ((uReal . (r - e1)) * (No_omega^ a)) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * (No_omega^ a)) where e2 is positive Real : verum } ] ; :: thesis: (uReal . r) * (No_omega^ a) == X
reconsider R = [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] as Surreal by Th49;
A2: R == uReal . r by Th56;
set N = No_omega^ a;
set RN = R * (No_omega^ a);
A3: R * (No_omega^ a) = [((comp ((L_ R),R,(No_omega^ a),(L_ (No_omega^ a)))) \/ (comp ((R_ R),R,(No_omega^ a),(R_ (No_omega^ a))))),((comp ((L_ R),R,(No_omega^ a),(R_ (No_omega^ a)))) \/ (comp ((R_ R),R,(No_omega^ a),(L_ (No_omega^ a)))))] by SURREALR:50;
A4: L_ (R * (No_omega^ a)) << {X}

proof

let x, w be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in L_ (R * (No_omega^ a)) or not w in {X} or not w <= x )
assume A5: ( x in L_ (R * (No_omega^ a)) & w in {X} ) ; :: thesis: not w <= x

per cases ( x in comp ((L_ R),R,(No_omega^ a),(L_ (No_omega^ a))) or x in comp ((R_ R),R,(No_omega^ a),(R_ (No_omega^ a))) ) by A3, A5, XBOOLE_0:def 3;

suppose x in comp ((L_ R),R,(No_omega^ a),(L_ (No_omega^ a))) ; :: thesis: not w <= x

then consider a1, b1 being Surreal such that
A6: ( x = ((a1 * (No_omega^ a)) + (R * b1)) - (a1 * b1) & a1 in L_ R & b1 in L_ (No_omega^ a) ) by SURREALR:def 15;
consider e1 being positive Real such that
A7: a1 = uReal . (r - e1) by A6;

per cases ( b1 = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ a & b1 = (No_omega^ xL) * (uReal . r) ) ) by A6, SURREALC:22;

suppose b1 = 0_No ; :: thesis: not w <= x

then ( x in L_ X & L_ X << {X} ) by A1, A6, A7, SURREALO:11;
hence not w <= x by A5; :: thesis: verum

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ a & b1 = (No_omega^ xL) * (uReal . r) ) ; :: thesis: not w <= x

then consider xL being Surreal, e2 being positive Real such that
A8: ( xL in L_ a & b1 = (No_omega^ xL) * (uReal . e2) ) ;
set NL = No_omega^ xL;
set E2 = uReal . e2;
A9: x = (a1 * (No_omega^ a)) + ((R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))))) by A6, A7, A8, SURREALR:37;
( - (uReal . (r - e1)) == uReal . (- (r - e1)) & - ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))) = (- (uReal . (r - e1))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALN:56, SURREALR:58;
then ( R * ((No_omega^ xL) * (uReal . e2)) == (uReal . r) * ((No_omega^ xL) * (uReal . e2)) & - ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))) == (uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2)) ) by Th56, SURREALR:54;
then ( (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2))) & ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2))) == ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALR:43, SURREALR:67;
then A10: (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) by SURREALO:9;
(uReal . r) + (uReal . (- (r - e1))) == uReal . (r + (- (r - e1))) by SURREALN:55;
then ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) == (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALR:54;
then (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by A10, SURREALO:9;
then A11: x == (a1 * (No_omega^ a)) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) by A9, SURREALR:32;
r - e1 = (r - (e1 / 2)) - (e1 / 2) ;
then a1 == (uReal . (r - (e1 / 2))) - (uReal . (e1 / 2)) by A7, Th32;
then ( a1 * (No_omega^ a) == ((uReal . (r - (e1 / 2))) + (- (uReal . (e1 / 2)))) * (No_omega^ a) & ((uReal . (r - (e1 / 2))) + (- (uReal . (e1 / 2)))) * (No_omega^ a) == ((uReal . (r - (e1 / 2))) * (No_omega^ a)) + ((- (uReal . (e1 / 2))) * (No_omega^ a)) ) by SURREALR:54, SURREALR:67;
then a1 * (No_omega^ a) == ((uReal . (r - (e1 / 2))) * (No_omega^ a)) + ((- (uReal . (e1 / 2))) * (No_omega^ a)) by SURREALO:9;
then a1 * (No_omega^ a) == ((uReal . (r - (e1 / 2))) * (No_omega^ a)) - ((uReal . (e1 / 2)) * (No_omega^ a)) by SURREALR:58;
then (a1 * (No_omega^ a)) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) == (((uReal . (r - (e1 / 2))) * (No_omega^ a)) - ((uReal . (e1 / 2)) * (No_omega^ a))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) by SURREALR:32;
then A12: ( x == (((uReal . (r - (e1 / 2))) * (No_omega^ a)) + (- ((uReal . (e1 / 2)) * (No_omega^ a)))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) & (((uReal . (r - (e1 / 2))) * (No_omega^ a)) + (- ((uReal . (e1 / 2)) * (No_omega^ a)))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) = ((uReal . (r - (e1 / 2))) * (No_omega^ a)) + (((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) - ((uReal . (e1 / 2)) * (No_omega^ a))) ) by A11, SURREALR:37, SURREALO:9;
( L_ a << {a} & a in {a} ) by SURREALO:11, TARSKI:def 1;
then No_omega^ xL infinitely< No_omega^ a by A8, SURREALC:25;
then No_omega^ xL infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then (No_omega^ xL) * (uReal . e2) infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) - ((uReal . (e1 / 2)) * (No_omega^ a)) < 0_No by SURREALR:46, SURREALC:9;
then ((uReal . (r - (e1 / 2))) * (No_omega^ a)) + (((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) - ((uReal . (e1 / 2)) * (No_omega^ a))) < ((uReal . (r - (e1 / 2))) * (No_omega^ a)) + 0_No by SURREALR:32;
then A13: x < (uReal . (r - (e1 / 2))) * (No_omega^ a) by A12, SURREALO:9;
( (uReal . (r - (e1 / 2))) * (No_omega^ a) in L_ X & L_ X << {X} ) by A1, SURREALO:11;
then (uReal . (r - (e1 / 2))) * (No_omega^ a) <= w by A5;
hence not w <= x by A13, SURREALO:9; :: thesis: verum

end;

end;

end;

suppose x in comp ((R_ R),R,(No_omega^ a),(R_ (No_omega^ a))) ; :: thesis: not w <= x

then consider a1, b1 being Surreal such that
A14: ( x = ((a1 * (No_omega^ a)) + (R * b1)) - (a1 * b1) & a1 in R_ R & b1 in R_ (No_omega^ a) ) by SURREALR:def 15;
consider e1 being positive Real such that
A15: a1 = uReal . (r + e1) by A14;
consider xL being Surreal, e2 being positive Real such that
A16: ( xL in R_ a & b1 = (No_omega^ xL) * (uReal . e2) ) by A14, SURREALC:23;
set NL = No_omega^ xL;
set E2 = uReal . e2;
A17: x = (a1 * (No_omega^ a)) + ((R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))))) by A14, A15, A16, SURREALR:37;
( - (uReal . (r + e1)) == uReal . (- (r + e1)) & - ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))) = (- (uReal . (r + e1))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALN:56, SURREALR:58;
then ( R * ((No_omega^ xL) * (uReal . e2)) == (uReal . r) * ((No_omega^ xL) * (uReal . e2)) & - ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))) == (uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2)) ) by Th56, SURREALR:54;
then ( (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2))) & ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2))) == ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALR:43, SURREALR:67;
then A18: (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) by SURREALO:9;
(uReal . r) + (uReal . (- (r + e1))) == uReal . (r + (- (r + e1))) by SURREALN:55;
then ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) == (uReal . (- e1)) * ((No_omega^ xL) * (uReal . e2)) by SURREALR:54;
then (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == (uReal . (- e1)) * ((No_omega^ xL) * (uReal . e2)) by A18, SURREALO:9;
then A19: x == (a1 * (No_omega^ a)) + ((uReal . (- e1)) * ((No_omega^ xL) * (uReal . e2))) by A17, SURREALR:32;
( (uReal . (- e1)) * ((No_omega^ xL) * (uReal . e2)) == (- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2)) & (- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2)) = - ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) ) by SURREALN:56, SURREALR:54, SURREALR:58;
then (a1 * (No_omega^ a)) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) == (a1 * (No_omega^ a)) + ((uReal . (- e1)) * ((No_omega^ xL) * (uReal . e2))) by SURREALR:32;
then A20: (a1 * (No_omega^ a)) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) == x by A19, SURREALO:9;
(r - e1) + (2 * e1) = r + e1 ;
then ( a1 * (No_omega^ a) == ((uReal . (r - e1)) + (uReal . (2 * e1))) * (No_omega^ a) & ((uReal . (r - e1)) + (uReal . (2 * e1))) * (No_omega^ a) == ((uReal . (r - e1)) * (No_omega^ a)) + ((uReal . (2 * e1)) * (No_omega^ a)) ) by A15, SURREALN:55, SURREALR:54, SURREALR:67;
then a1 * (No_omega^ a) == ((uReal . (r - e1)) * (No_omega^ a)) + ((uReal . (2 * e1)) * (No_omega^ a)) by SURREALO:9;
then (a1 * (No_omega^ a)) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) == (((uReal . (r - e1)) * (No_omega^ a)) + ((uReal . (2 * e1)) * (No_omega^ a))) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) by SURREALR:32;
then A21: ( x == (((uReal . (r - e1)) * (No_omega^ a)) + ((uReal . (2 * e1)) * (No_omega^ a))) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) & (((uReal . (r - e1)) * (No_omega^ a)) + ((uReal . (2 * e1)) * (No_omega^ a))) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) = ((uReal . (r - e1)) * (No_omega^ a)) + (((uReal . (2 * e1)) * (No_omega^ a)) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))))) ) by A20, SURREALR:37, SURREALO:9;
( a in {a} & {a} << R_ a ) by TARSKI:def 1, SURREALO:11;
then No_omega^ a infinitely< No_omega^ xL by A16, SURREALC:25;
then No_omega^ a infinitely< (No_omega^ xL) * (uReal . e2) by SURREALC:13;
then No_omega^ a infinitely< (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALC:13;
then (uReal . (2 * e1)) * (No_omega^ a) infinitely< (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALC:13;
then ((uReal . (2 * e1)) * (No_omega^ a)) - ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) < 0_No by SURREALR:46, SURREALC:9;
then ((uReal . (r - e1)) * (No_omega^ a)) + (((uReal . (2 * e1)) * (No_omega^ a)) + (- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))))) < ((uReal . (r - e1)) * (No_omega^ a)) + 0_No by SURREALR:32;
then A22: x < (uReal . (r - e1)) * (No_omega^ a) by A21, SURREALO:9;
( (uReal . (r - e1)) * (No_omega^ a) in L_ X & L_ X << {X} ) by A1, SURREALO:11;
then (uReal . (r - e1)) * (No_omega^ a) <= w by A5;
hence not w <= x by A22, SURREALO:9; :: thesis: verum

end;

end;

end;

A23: {(R * (No_omega^ a))} << R_ X

proof

let x, y be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not x in {(R * (No_omega^ a))} or not y in R_ X or not y <= x )
assume A24: ( x in {(R * (No_omega^ a))} & y in R_ X ) ; :: thesis: not y <= x
consider e being positive Real such that
A25: y = (uReal . (r + e)) * (No_omega^ a) by A1, A24;
A26: No_omega^ a is positive ;
r < r + e by XREAL_1:29;
then R < uReal . (r + e) by A2, SURREALO:9, SURREALN:51;
then ( x = R * (No_omega^ a) & R * (No_omega^ a) < (uReal . (r + e)) * (No_omega^ a) ) by A24, TARSKI:def 1, A26, SURREALR:70;
hence not y <= x by A25; :: thesis: verum

end;

A27: L_ X << {(R * (No_omega^ a))}

proof

let y, x be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not y in L_ X or not x in {(R * (No_omega^ a))} or not x <= y )
assume A28: ( y in L_ X & x in {(R * (No_omega^ a))} ) ; :: thesis: not x <= y
consider e being positive Real such that
A29: y = (uReal . (r - e)) * (No_omega^ a) by A1, A28;
A30: No_omega^ a is positive ;
r + (- e) < r by XREAL_1:30;
then R > uReal . (r - e) by A2, SURREALO:9, SURREALN:51;
then ( x = R * (No_omega^ a) & R * (No_omega^ a) > (uReal . (r - e)) * (No_omega^ a) ) by A28, TARSKI:def 1, A30, SURREALR:70;
hence not x <= y by A29; :: thesis: verum

end;

A31: {X} << R_ (R * (No_omega^ a))

proof

let w, x be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not w in {X} or not x in R_ (R * (No_omega^ a)) or not x <= w )
assume A32: ( w in {X} & x in R_ (R * (No_omega^ a)) ) ; :: thesis: not x <= w

per cases ( x in comp ((R_ R),R,(No_omega^ a),(L_ (No_omega^ a))) or x in comp ((L_ R),R,(No_omega^ a),(R_ (No_omega^ a))) ) by A3, A32, XBOOLE_0:def 3;

suppose x in comp ((R_ R),R,(No_omega^ a),(L_ (No_omega^ a))) ; :: thesis: not x <= w

then consider a1, b1 being Surreal such that
A33: ( x = ((a1 * (No_omega^ a)) + (R * b1)) - (a1 * b1) & a1 in R_ R & b1 in L_ (No_omega^ a) ) by SURREALR:def 15;
consider e1 being positive Real such that
A34: a1 = uReal . (r + e1) by A33;

per cases ( b1 = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ a & b1 = (No_omega^ xL) * (uReal . r) ) ) by A33, SURREALC:22;

suppose b1 = 0_No ; :: thesis: not x <= w

then ( x in R_ X & {X} << R_ X ) by A1, A33, A34, SURREALO:11;
hence not x <= w by A32; :: thesis: verum

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ a & b1 = (No_omega^ xL) * (uReal . r) ) ; :: thesis: not x <= w

then consider xL being Surreal, e2 being positive Real such that
A35: ( xL in L_ a & b1 = (No_omega^ xL) * (uReal . e2) ) ;
set NL = No_omega^ xL;
set E2 = uReal . e2;
A36: x = (a1 * (No_omega^ a)) + ((R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))))) by A33, A34, A35, SURREALR:37;
( - (uReal . (r + e1)) == uReal . (- (r + e1)) & - ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))) = (- (uReal . (r + e1))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALN:56, SURREALR:58;
then ( R * ((No_omega^ xL) * (uReal . e2)) == (uReal . r) * ((No_omega^ xL) * (uReal . e2)) & - ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2))) == (uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2)) ) by Th56, SURREALR:54;
then ( (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2))) & ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r + e1))) * ((No_omega^ xL) * (uReal . e2))) == ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALR:43, SURREALR:67;
then A37: (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) by SURREALO:9;
(uReal . r) + (uReal . (- (r + e1))) == uReal . (r + (- (r + e1))) by SURREALN:55;
then ( (uReal . r) + (uReal . (- (r + e1))) == uReal . (- e1) & uReal . (- e1) == - (uReal . e1) ) by SURREALN:56;
then (uReal . r) + (uReal . (- (r + e1))) == - (uReal . e1) by SURREALO:9;
then ((uReal . r) + (uReal . (- (r + e1)))) * ((No_omega^ xL) * (uReal . e2)) == (- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2)) by SURREALR:54;
then (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r + e1)) * ((No_omega^ xL) * (uReal . e2)))) == (- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2)) by A37, SURREALO:9;
then A38: x == (a1 * (No_omega^ a)) + ((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) by A36, SURREALR:32;
r + e1 = (r + (e1 / 2)) + (e1 / 2) ;
then ( a1 * (No_omega^ a) == ((uReal . (r + (e1 / 2))) + (uReal . (e1 / 2))) * (No_omega^ a) & ((uReal . (r + (e1 / 2))) + (uReal . (e1 / 2))) * (No_omega^ a) == ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((uReal . (e1 / 2)) * (No_omega^ a)) ) by A34, SURREALN:55, SURREALR:54, SURREALR:67;
then a1 * (No_omega^ a) == ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((uReal . (e1 / 2)) * (No_omega^ a)) by SURREALO:9;
then (a1 * (No_omega^ a)) + ((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) == (((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((uReal . (e1 / 2)) * (No_omega^ a))) + ((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) by SURREALR:32;
then A39: ( x == (((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((uReal . (e1 / 2)) * (No_omega^ a))) + ((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) & (((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((uReal . (e1 / 2)) * (No_omega^ a))) + ((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) = ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + (((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (e1 / 2)) * (No_omega^ a))) & ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + (((- (uReal . e1)) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (e1 / 2)) * (No_omega^ a))) = ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) + ((uReal . (e1 / 2)) * (No_omega^ a))) ) by A38, SURREALR:37, SURREALR:58, SURREALO:9;
( L_ a << {a} & a in {a} ) by SURREALO:11, TARSKI:def 1;
then No_omega^ xL infinitely< No_omega^ a by A35, SURREALC:25;
then No_omega^ xL infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then (No_omega^ xL) * (uReal . e2) infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) infinitely< (uReal . (e1 / 2)) * (No_omega^ a) by SURREALC:13;
then ((uReal . (e1 / 2)) * (No_omega^ a)) - ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) > 0_No by SURREALR:45, SURREALC:9;
then ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + ((- ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) + ((uReal . (e1 / 2)) * (No_omega^ a))) > ((uReal . (r + (e1 / 2))) * (No_omega^ a)) + 0_No by SURREALR:32;
then A40: x > (uReal . (r + (e1 / 2))) * (No_omega^ a) by A39, SURREALO:9;
( (uReal . (r + (e1 / 2))) * (No_omega^ a) in R_ X & R_ X >> {X} ) by A1, SURREALO:11;
then (uReal . (r + (e1 / 2))) * (No_omega^ a) > w by A32;
then (uReal . (r + (e1 / 2))) * (No_omega^ a) >= w by SURREALO:6;
hence not x <= w by A40, SURREALO:9; :: thesis: verum

end;

end;

end;

suppose x in comp ((L_ R),R,(No_omega^ a),(R_ (No_omega^ a))) ; :: thesis: not x <= w

then consider a1, b1 being Surreal such that
A41: ( x = ((a1 * (No_omega^ a)) + (R * b1)) - (a1 * b1) & a1 in L_ R & b1 in R_ (No_omega^ a) ) by SURREALR:def 15;
consider e1 being positive Real such that
A42: a1 = uReal . (r - e1) by A41;
consider xL being Surreal, e2 being positive Real such that
A43: ( xL in R_ a & b1 = (No_omega^ xL) * (uReal . e2) ) by A41, SURREALC:23;
set NL = No_omega^ xL;
set E2 = uReal . e2;
A44: x = (a1 * (No_omega^ a)) + ((R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))))) by A41, A42, A43, SURREALR:37;
( - (uReal . (r - e1)) == uReal . (- (r - e1)) & - ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))) = (- (uReal . (r - e1))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALN:56, SURREALR:58;
then ( R * ((No_omega^ xL) * (uReal . e2)) == (uReal . r) * ((No_omega^ xL) * (uReal . e2)) & - ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2))) == (uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2)) ) by Th56, SURREALR:54;
then ( (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2))) & ((uReal . r) * ((No_omega^ xL) * (uReal . e2))) + ((uReal . (- (r - e1))) * ((No_omega^ xL) * (uReal . e2))) == ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) ) by SURREALR:43, SURREALR:67;
then A45: (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) by SURREALO:9;
(uReal . r) + (uReal . (- (r - e1))) == uReal . (r + (- (r - e1))) by SURREALN:55;
then ((uReal . r) + (uReal . (- (r - e1)))) * ((No_omega^ xL) * (uReal . e2)) == (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALR:54;
then A46: (R * ((No_omega^ xL) * (uReal . e2))) + (- ((uReal . (r - e1)) * ((No_omega^ xL) * (uReal . e2)))) == (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by A45, SURREALO:9;
A47: (a1 * (No_omega^ a)) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) == x by A46, A44, SURREALR:32;
(r + e1) - (2 * e1) = r - e1 ;
then ( a1 * (No_omega^ a) == ((uReal . (r + e1)) - (uReal . (2 * e1))) * (No_omega^ a) & ((uReal . (r + e1)) - (uReal . (2 * e1))) * (No_omega^ a) == ((uReal . (r + e1)) * (No_omega^ a)) + ((- (uReal . (2 * e1))) * (No_omega^ a)) ) by Th32, A42, SURREALR:54, SURREALR:67;
then a1 * (No_omega^ a) == ((uReal . (r + e1)) * (No_omega^ a)) + ((- (uReal . (2 * e1))) * (No_omega^ a)) by SURREALO:9;
then a1 * (No_omega^ a) == ((uReal . (r + e1)) * (No_omega^ a)) + (- ((uReal . (2 * e1)) * (No_omega^ a))) by SURREALR:58;
then (a1 * (No_omega^ a)) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) == (((uReal . (r + e1)) * (No_omega^ a)) + (- ((uReal . (2 * e1)) * (No_omega^ a)))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) by SURREALR:32;
then A48: ( x == (((uReal . (r + e1)) * (No_omega^ a)) + (- ((uReal . (2 * e1)) * (No_omega^ a)))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) & (((uReal . (r + e1)) * (No_omega^ a)) + (- ((uReal . (2 * e1)) * (No_omega^ a)))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) = ((uReal . (r + e1)) * (No_omega^ a)) + ((- ((uReal . (2 * e1)) * (No_omega^ a))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) ) by A47, SURREALR:37, SURREALO:9;
( a in {a} & {a} << R_ a ) by TARSKI:def 1, SURREALO:11;
then No_omega^ a infinitely< No_omega^ xL by A43, SURREALC:25;
then No_omega^ a infinitely< (No_omega^ xL) * (uReal . e2) by SURREALC:13;
then No_omega^ a infinitely< (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALC:13;
then (uReal . (2 * e1)) * (No_omega^ a) infinitely< (uReal . e1) * ((No_omega^ xL) * (uReal . e2)) by SURREALC:13;
then 0_No < ((uReal . e1) * ((No_omega^ xL) * (uReal . e2))) - ((uReal . (2 * e1)) * (No_omega^ a)) by SURREALR:45, SURREALC:9;
then ((uReal . (r + e1)) * (No_omega^ a)) + ((- ((uReal . (2 * e1)) * (No_omega^ a))) + ((uReal . e1) * ((No_omega^ xL) * (uReal . e2)))) > ((uReal . (r + e1)) * (No_omega^ a)) + 0_No by SURREALR:32;
then x > (uReal . (r + e1)) * (No_omega^ a) by A48, SURREALO:9;
then A49: x >= (uReal . (r + e1)) * (No_omega^ a) by SURREALO:6;
( (uReal . (r + e1)) * (No_omega^ a) in R_ X & {X} << R_ X ) by A1, SURREALO:11;
hence not x <= w by A32, A49, SURREALO:9; :: thesis: verum

end;

end;

end;

A50: X == R * (No_omega^ a) by A23, A4, SURREAL0:43, A27, A31;
R * (No_omega^ a) == (uReal . r) * (No_omega^ a) by Th56, SURREALR:54;
hence (uReal . r) * (No_omega^ a) == X by A50, SURREALO:9; :: thesis: verum