let PM be MetrStruct ; :: thesis: the carrier of (TopSpaceMetr PM) = the carrier of PM
the carrier of (TopSpaceMetr PM) = the carrier of TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;
hence the carrier of (TopSpaceMetr PM) = the carrier of PM ; :: thesis: verum