let X be RealUnitarySpace; :: thesis: for x, y, z being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
let x, y, z be Point of X; :: thesis: dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
dist ((x - z),(y - z)) = ||.((x - z) + (z - y)).|| by RLVECT_1:33
.= ||.((- (z - x)) + (z - y)).|| by RLVECT_1:33 ;
then dist ((x - z),(y - z)) <= ||.(- (z - x)).|| + ||.(z - y).|| by Th30;
hence dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y)) by Th31; :: thesis: verum