let X be ComplexUnitarySpace; 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; 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 Th41;
hence
dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
by Th42; verum