for V being non empty right_complementable triangle Abelian add-associative right_zeroed translatible RLSMetrStruct
for v, w being Element of V holds Norm (v + w) <= (Norm v) + (Norm w)