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