let x, y, z, t be Real; :: thesis: ( |.x.| <= z & |.y.| <= t implies |.(x + y).| <= z + t )
assume ( |.x.| <= z & |.y.| <= t ) ; :: thesis: |.(x + y).| <= z + t
then ( |.(x + y).| <= |.x.| + |.y.| & |.x.| + |.y.| <= z + t ) by COMPLEX1:56, XREAL_1:7;
hence |.(x + y).| <= z + t by XXREAL_0:2; :: thesis: verum