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)) = ||.(((- u) + (- v)) + (x + y)).|| by RLVECT_1:31
.= ||.((x + ((- u) + (- v))) + y).|| by RLVECT_1:def 3
.= ||.(((x - u) + (- v)) + y).|| by RLVECT_1:def 3
.= ||.((x - u) + (y - v)).|| by RLVECT_1:def 3 ;
hence dist ((x + y),(u + v)) <= (dist (x,u)) + (dist (y,v)) by Th41; :: thesis: verum