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