let r1, r2 be Real; :: thesis: (L_ (sReal . r1)) ++ {(sReal . r2)} << {(sReal . (r1 + r2))}
let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in (L_ (sReal . r1)) ++ {(sReal . r2)} or not b in {(sReal . (r1 + r2))} or not b <= a )
assume A1: ( a in (L_ (sReal . r1)) ++ {(sReal . r2)} & b in {(sReal . (r1 + r2))} ) ; :: thesis: not b <= a
consider a1, a2 being Surreal such that
A2: ( a1 in L_ (sReal . r1) & a2 in {(sReal . r2)} & a = a1 + a2 ) by A1, SURREALR:def 8;
A3: a2 = sReal . r2 by A2, TARSKI:def 1;
consider n being Nat such that
A4: a1 = uDyadic . ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) by A2, Th42;
set d = [/((r1 * (2 |^ n)) - 1)\] / (2 |^ n);
0 < r1 - ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) by Th41, XREAL_1:50;
then r2 + 0 < (r1 - ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n))) + r2 by XREAL_1:8;
then consider k being Nat such that
A5: [\((r2 * (2 |^ k)) + 1)/] / (2 |^ k) < (r1 - ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n))) + r2 by Th53;
A6: a < a1 + (uDyadic . ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) by A3, Th44, A2, SURREALR:44;
( a1 + (uDyadic . ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) == uDyadic . (([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) & uDyadic . (([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) == sReal . (([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) ) by A4, Th39, Th46;
then a1 + (uDyadic . ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) == sReal . (([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) by SURREALO:4;
then A7: a <= sReal . (([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k))) by A6, SURREALO:4;
( ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ([\((r2 * (2 |^ k)) + 1)/] / (2 |^ k)) < ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ((r1 - ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n))) + r2) & ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n)) + ((r1 - ([/((r1 * (2 |^ n)) - 1)\] / (2 |^ n))) + r2) = r1 + r2 ) by A5, XREAL_1:6;
then a < sReal . (r1 + r2) by Th50, A7, SURREALO:4;
hence not b <= a by A1, TARSKI:def 1; :: thesis: verum