let CNS be ComplexNormSpace; :: thesis: for x, y, w being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
let x, y, w be Point of CNS; :: thesis: ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
x - w = x + (H₁(CNS) + (- w)) by RLVECT_1:4
.= x + (((- y) + y) + (- w)) by RLVECT_1:5
.= x + ((- y) + (y + (- w))) by RLVECT_1:def 3
.= (x - y) + (y - w) by RLVECT_1:def 3 ;
hence ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).|| by Def13; :: thesis: verum