let V be non empty right_complementable Abelian add-associative right_zeroed triangle 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:16;
then Norm (v + w) <= (Norm v) + (dist (0. V),(w + ((- v) + v))) by RLVECT_1:def 6;
then Norm (v + w) <= (Norm v) + (dist (0. V),(w + (0. V))) by RLVECT_1:16;
hence Norm (v + w) <= (Norm v) + (Norm w) by RLVECT_1:10; :: thesis: verum