theorem :: CSSPACE:51

for X being ComplexUnitarySpace
for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))