let X be RealUnitarySpace; :: 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:10
.= ||.((x - z) + (y - y)).|| by RLVECT_1:28
.= ||.(x - (z - (y - y))).|| by RLVECT_1:43
.= ||.(x - (y + (z - y))).|| by RLVECT_1:43
.= ||.((x - y) - (z - y)).|| by RLVECT_1:41
.= ||.((x - y) + (y - z)).|| by RLVECT_1:47 ;
hence dist (x,z) <= (dist (x,y)) + (dist (y,z)) by Th36; :: thesis: verum