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:43
.= ||.((x - (u + y)) + v).|| by RLVECT_1:41
.= ||.(((x - u) - y) + v).|| by RLVECT_1:41
.= ||.((x - u) - (y - v)).|| by RLVECT_1:43
.= ||.((x - u) + (- (y - v))).|| ;
then dist (x - y),(u - v) <= ||.(x - u).|| + ||.(- (y - v)).|| by Th48;
hence dist (x - y),(u - v) <= (dist x,u) + (dist y,v) by Th49; :: thesis: verum