let x, y, z, e be Real; :: thesis: ( abs (x - y) < e / 2 & abs (y - z) < e / 2 implies abs (x - z) < e )
assume ( abs (x - y) < e / 2 & abs (y - z) < e / 2 ) ; :: thesis: abs (x - z) < e
then ( abs ((x - y) + (y - z)) <= (abs (x - y)) + (abs (y - z)) & (abs (x - y)) + (abs (y - z)) < (e / 2) + (e / 2) ) by COMPLEX1:56, XREAL_1:8;
hence abs (x - z) < e by XXREAL_0:2; :: thesis: verum