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

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

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

end;

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