let x, y, z be Surreal; :: thesis: ( x infinitely< z & y infinitely< z implies x + y infinitely< z )
assume A1: ( x infinitely< z & y infinitely< z ) ; :: thesis: x + y infinitely< z
let r be positive Real; :: according to SURREALC:def 3 :: thesis: (x + y) * (uReal . r) < z
set R = uReal . r;
set H = uReal . (1 / 2);
A2: (1 / 2) + (1 / 2) = 1 ;
( x infinitely< z * (uReal . (1 / 2)) & y infinitely< z * (uReal . (1 / 2)) ) by A1, Th13;
then ( x * (uReal . r) < z * (uReal . (1 / 2)) & y * (uReal . r) <= z * (uReal . (1 / 2)) ) ;
then A3: (x * (uReal . r)) + (y * (uReal . r)) < (z * (uReal . (1 / 2))) + (z * (uReal . (1 / 2))) by SURREALR:44;
( (z * (uReal . (1 / 2))) + (z * (uReal . (1 / 2))) == z * ((uReal . (1 / 2)) + (uReal . (1 / 2))) & z * ((uReal . (1 / 2)) + (uReal . (1 / 2))) == z * 1_No & z * 1_No = z ) by A2, SURREALN:55, SURREALN:48, SURREALR:51, SURREALR:67;
then (z * (uReal . (1 / 2))) + (z * (uReal . (1 / 2))) == z by SURREALO:4;
then ( (x + y) * (uReal . r) == (x * (uReal . r)) + (y * (uReal . r)) & (x * (uReal . r)) + (y * (uReal . r)) < z ) by A3, SURREALO:4, SURREALR:67;
hence (x + y) * (uReal . r) < z by SURREALO:4; :: thesis: verum