let M be MetrStruct ; :: thesis: ( the carrier of M = the carrier of (TopSpaceMetr M) & the topology of (TopSpaceMetr M) = Family_open_set M )
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
hence ( the carrier of M = the carrier of (TopSpaceMetr M) & the topology of (TopSpaceMetr M) = Family_open_set M ) ; :: thesis: verum