set MS = the non empty strict MetrSpace;
take TS = TopSpaceMetr the non empty strict MetrSpace; :: thesis: ( TS is strict & TS is metrizable )
reconsider f = the distance of the non empty strict MetrSpace 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 8 :: 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 Th35; :: 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 Def7; :: thesis: verum