let V be non empty right_complementable triangle Abelian add-associative right_zeroed translatible RLSMetrStruct ; :: thesis: for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w)
let v, w be Element of V; :: thesis: Norm (v + w) <= (Norm v) + (Norm w)
Norm (v + w) <= (dist ((0. V),v)) + (dist (v,(v + w))) by METRIC_1:4;
then Norm (v + w) <= (Norm v) + (dist ((v + (- v)),((v + w) + (- v)))) by Def6;
then Norm (v + w) <= (Norm v) + (dist ((0. V),((v + w) + (- v)))) by RLVECT_1:5;
then Norm (v + w) <= (Norm v) + (dist ((0. V),(w + ((- v) + v)))) by RLVECT_1:def 3;
then Norm (v + w) <= (Norm v) + (dist ((0. V),(w + (0. V)))) by RLVECT_1:5;
hence Norm (v + w) <= (Norm v) + (Norm w) by RLVECT_1:4; :: thesis: verum