per cases ( M is empty or not M is empty ) ;

suppose M is empty ; :: thesis: TopSpaceMetr M is metrizable

then TopSpaceMetr M is empty ;
hence TopSpaceMetr M is metrizable ; :: thesis: verum

end;

suppose not M is empty ; :: thesis: TopSpaceMetr M is metrizable

then reconsider m = M as non empty MetrSpace ;
set TM = TopSpaceMetr M;
reconsider CM = [#] M as non empty Subset of m ;
reconsider CTM = [#] (TopSpaceMetr M) as Subset of (TopSpaceMetr M) ;
set TMM = TopSpaceMetr (m | CM);
A8: [#] (m | CM) = CM by TOPMETR:def 2;
then reconsider D = the distance of (m | CM) as Function of [: the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M):],REAL ;
take D ; :: according to PCOMPS_1:def 8 :: thesis: ( D is_metric_of the carrier of (TopSpaceMetr M) & Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) = the topology of (TopSpaceMetr M) )
A9: D is_metric_of the carrier of (TopSpaceMetr M) by A8, PCOMPS_1:35;
( (TopSpaceMetr M) | CTM = TopSpaceMetr (m | CM) & TopSpaceMetr M is SubSpace of TopSpaceMetr M ) by HAUSDORF:16, TSEP_1:2;
then the topology of (TopSpaceMetr M) = the topology of (TopSpaceMetr (m | CM)) by A8, TSEP_1:5
.= Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) by A8, A9, PCOMPS_1:def 7 ;
hence ( D is_metric_of the carrier of (TopSpaceMetr M) & Family_open_set (SpaceMetr ( the carrier of (TopSpaceMetr M),D)) = the topology of (TopSpaceMetr M) ) by A8, PCOMPS_1:35; :: thesis: verum

end;

end;