let X be ComplexUnitarySpace; :: thesis: for x, z, y being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
let x, z, y be Point of X; :: thesis: dist (x,z) <= (dist (x,y)) + (dist (y,z))
dist (x,z) = ||.((x - z) + H₁(X)).|| by RLVECT_1:4
.= ||.((x - z) + (y - y)).|| by RLVECT_1:15
.= ||.(x - (z - (y - y))).|| by RLVECT_1:29
.= ||.(x - (y + (z - y))).|| by RLVECT_1:29
.= ||.((x - y) - (z - y)).|| by RLVECT_1:27
.= ||.((x - y) + (y - z)).|| by RLVECT_1:33 ;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th48; :: thesis: verum