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