SpaceMetr (REAL n),(Pitag_dist n) = MetrStruct(# (REAL n),(Pitag_dist n) #) by Th24, PCOMPS_1:def 8;
hence MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrSpace ; :: thesis: verum