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