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);
A10: [#] (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 9 :: 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) )
A11: D is_metric_of the carrier of (TopSpaceMetr M) by A10, PCOMPS_1:39;
( (TopSpaceMetr M) | CTM = TopSpaceMetr (m | CM) & TopSpaceMetr M is SubSpace of TopSpaceMetr M ) by HAUSDORF:18, TSEP_1:2;
then the topology of (TopSpaceMetr M) = the topology of (TopSpaceMetr (m | CM)) by A10, TSEP_1:5
.= Family_open_set (SpaceMetr the carrier of (TopSpaceMetr M),D) by A10, A11, PCOMPS_1:def 8 ;
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 A10, PCOMPS_1:39; :: thesis: verum

end;

end;