let X be ComplexNormSpace; :: thesis: for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; :: thesis: for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; :: thesis: ( ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 implies ||.(x - y).|| < e )
assume that
A1: ||.(x - z).|| < e / 2 and
A2: ||.(y - z).|| < e / 2 ; :: thesis: ||.(x - y).|| < e
||.(- (y - z)).|| < e / 2 by A2, CLVECT_1:103;
then ||.(z - y).|| < e / 2 by RLVECT_1:33;
hence ||.(x - y).|| < e by A1, Lm1; :: thesis: verum