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