consider MS being non empty strict MetrSpace;
take TS = TopSpaceMetr MS; :: thesis: ( TS is strict & TS is metrizable )
reconsider f = the distance of MS as Function of [:the carrier of TS,the carrier of TS:],REAL ;
thus TS is strict ; :: thesis: TS is metrizable
take f ; :: according to PCOMPS_1:def 9 :: thesis: ( f is_metric_of the carrier of TS & Family_open_set (SpaceMetr the carrier of TS,f) = the topology of TS )
thus f is_metric_of the carrier of TS by Th39; :: thesis: Family_open_set (SpaceMetr the carrier of TS,f) = the topology of TS
hence Family_open_set (SpaceMetr the carrier of TS,f) = the topology of TS by Def8; :: thesis: verum