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

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

let a, b be Element of X; :: thesis: (distance_by_norm_of X) . (a,b) = (distance_by_norm_of X) . (b,a)
thus (distance_by_norm_of X) . (a,b) = ||.(a - b).|| by Def1
.= ||.(b - a).|| by NORMSP_1:7
.= (distance_by_norm_of X) . (b,a) by Def1 ; :: thesis: verum

end;

hence the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric ; :: thesis: verum