let x, z, y, t be real number ; :: thesis: ( abs x <= z & abs y <= t implies abs (x + y) <= z + t )
assume that
A1: abs x <= z and
A2: abs y <= t ; :: thesis: abs (x + y) <= z + t
A3: abs (x + y) <= (abs x) + (abs y) by COMPLEX1:142;
(abs x) + (abs y) <= z + t by A1, A2, XREAL_1:9;
hence abs (x + y) <= z + t by A3, XXREAL_0:2; :: thesis: verum