let RNS be RealNormSpace; :: thesis: for x, y being Point of RNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
let x, y be Point of RNS; :: thesis: ||.(x - y).|| <= ||.x.|| + ||.y.||
||.(x - y).|| <= ||.x.|| + ||.(- y).|| by Def1;
hence ||.(x - y).|| <= ||.x.|| + ||.y.|| by Th2; :: thesis: verum