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

now

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:11
.= (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 by METRIC_1:def 5; :: thesis: verum