let X be RealUnitarySpace; :: thesis: for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
let x, y, z 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 Th30; :: thesis: verum