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

now :: thesis: for a, b, c being Element of X holds (distance_by_norm_of X) . (a,c) <= ((distance_by_norm_of X) . (a,b)) + ((distance_by_norm_of X) . (b,c))

let a, b, c be Element 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:10;
||.(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 ; :: thesis: verum