let CNS be ComplexNormSpace; :: thesis: for x, w, y being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
let x, w, y be Point of CNS; :: thesis: ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||
x - w = x + (H₁(CNS) + (- w)) by RLVECT_1:10
.= x + (((- y) + y) + (- w)) by RLVECT_1:16
.= x + ((- y) + (y + (- w))) by RLVECT_1:def 6
.= (x - y) + (y - w) by RLVECT_1:def 6 ;
hence ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).|| by Def14; :: thesis: verum