let X be ComplexNormSpace; :: thesis: for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; :: thesis: for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; :: thesis: ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 implies ||.(x - y).|| < e )
assume ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 ) ; :: thesis: ||.(x - y).|| < e
then ||.(x - z).|| + ||.(z - y).|| < (e / 2) + (e / 2) by XREAL_1:8;
then ||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||) < (||.(x - z).|| + ||.(z - y).||) + e by CLVECT_1:111, XREAL_1:8;
then (||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8;
hence ||.(x - y).|| < e ; :: thesis: verum