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