let X be ComplexUnitarySpace; :: thesis: for x, y, u, v being Point of X holds dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
let x, y, u, v be Point of X; :: thesis: dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v))
dist ((x - y),(u - v)) = ||.(((x - y) - u) + v).|| by RLVECT_1:29
.= ||.((x - (u + y)) + v).|| by RLVECT_1:27
.= ||.(((x - u) - y) + v).|| by RLVECT_1:27
.= ||.((x - u) - (y - v)).|| by RLVECT_1:29
.= ||.((x - u) + (- (y - v))).|| ;
then dist ((x - y),(u - v)) <= ||.(x - u).|| + ||.(- (y - v)).|| by Th41;
hence dist ((x - y),(u - v)) <= (dist (x,u)) + (dist (y,v)) by Th42; :: thesis: verum