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