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

suppose Am is empty ; :: thesis: TM | Am is metrizable

hence TM | Am is metrizable ; :: thesis: verum

end;

suppose A1: not Am is empty ; :: thesis: TM | Am is metrizable

consider metr being Function of [: the carrier of TM, the carrier of TM:],REAL such that
A2: metr is_metric_of the carrier of TM and
A3: Family_open_set (SpaceMetr ( the carrier of TM,metr)) = the topology of TM by PCOMPS_1:def 8;
A4: not TM is empty by A1;
then reconsider TMM = SpaceMetr ( the carrier of TM,metr) as non empty MetrSpace by A2, PCOMPS_1:36;
reconsider Atm = Am as non empty Subset of TMM by A1, A2, A4, PCOMPS_2:4;
reconsider ATM = Atm as non empty Subset of (TopSpaceMetr TMM) ;
( TM is SubSpace of TM & the carrier of (TopSpaceMetr TMM) = the carrier of TM ) by A2, A4, PCOMPS_2:4, TSEP_1:2;
then TopSpaceMetr TMM is SubSpace of TM by A3, TMAP_1:6;
then A5: (TopSpaceMetr TMM) | ATM is SubSpace of TM by TSEP_1:7;
( (TopSpaceMetr TMM) | ATM = TopSpaceMetr (TMM | Atm) & [#] ((TopSpaceMetr TMM) | ATM) = ATM ) by HAUSDORF:16, PRE_TOPC:def 5;
hence TM | Am is metrizable by A5, PRE_TOPC:def 5; :: thesis: verum

end;

end;