let X be ComplexUnitarySpace; :: thesis: for x, z, y being Point of X holds dist (x - z),(y - z) <= (dist z,x) + (dist z,y)
let x, z, y 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:47
.= ||.((- (z - x)) + (z - y)).|| by RLVECT_1:47 ;
then dist (x - z),(y - z) <= ||.(- (z - x)).|| + ||.(z - y).|| by Th48;
hence dist (x - z),(y - z) <= (dist z,x) + (dist z,y) by Th49; :: thesis: verum