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 A4: (|.x.| * (uReal . r)) + (|.y.| * (uReal . r)) < z by A3, SURREALO:4;
A5: 0_No <= uReal . r by SURREALI:def 8;
( |.(x + y).| * (uReal . r) <= (|.x.| + |.y.|) * (uReal . r) & (|.x.| + |.y.|) * (uReal . r) == (|.x.| * (uReal . r)) + (|.y.| * (uReal . r)) ) by Th37, A5, SURREALR:75, SURREALR:67;
then |.(x + y).| * (uReal . r) <= (|.x.| * (uReal . r)) + (|.y.| * (uReal . r)) by SURREALO:4;
hence |.(x + y).| * (uReal . r) < z by A4, SURREALO:4; :: thesis: verum