let X be RealNormSpace; :: thesis: the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle

now

let a, b, c be Element of the carrier of X; :: thesis: (distance_by_norm_of X) . a,c <= ((distance_by_norm_of X) . a,b) + ((distance_by_norm_of X) . b,c)
A1: ||.(a - c).|| <= ||.(a - b).|| + ||.(b - c).|| by NORMSP_1:14;
||.(a - b).|| + ||.(b - c).|| = ||.(a - b).|| + ((distance_by_norm_of X) . b,c) by Def1
.= ((distance_by_norm_of X) . a,b) + ((distance_by_norm_of X) . b,c) by Def1 ;
hence (distance_by_norm_of X) . a,c <= ((distance_by_norm_of X) . a,b) + ((distance_by_norm_of X) . b,c) by A1, Def1; :: thesis: verum

end;

hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle by METRIC_1:def 6; :: thesis: verum