let X be RealNormSpace; :: 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 )
A1: ||.(z - y).|| = ||.(y - z).|| by NORMSP_1:7;
assume ( ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 ) ; :: thesis: ||.(x - y).|| < e
then ||.(x - z).|| + ||.(y - z).|| < (e / 2) + (e / 2) by XREAL_1:8;
then ||.(x - y).|| + (||.(x - z).|| + ||.(y - z).||) < (||.(x - z).|| + ||.(z - y).||) + e by NORMSP_1:10, XREAL_1:8;
then (||.(x - y).|| + (||.(x - z).|| + ||.(y - z).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8;
hence ||.(x - y).|| < e by A1; :: thesis: verum