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

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