let x, y be Surreal; :: thesis: |.(x + y).| <= |.x.| + |.y.|
( - |.x.| <= x & x <= |.x.| & - |.y.| <= y & y <= |.y.| ) by Th34;
then ( - (|.x.| + |.y.|) = (- |.x.|) + (- |.y.|) & (- |.x.|) + (- |.y.|) <= x + y & x + y <= |.x.| + |.y.| ) by SURREALR:40, SURREALR:43;
hence |.(x + y).| <= |.x.| + |.y.| by Th35; :: thesis: verum