let RNS be RealNormSpace; :: thesis: for x, y, z being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
let x, y, z be Point of RNS; :: thesis: ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
x - z = x + (H₁(RNS) + (- z))
.= x + (((- y) + y) + (- z)) by RLVECT_1:5
.= x + ((- y) + (y + (- z))) by RLVECT_1:def 3
.= (x - y) + (y - z) by RLVECT_1:def 3 ;
hence ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).|| by Def1; :: thesis: verum