let PT be non empty TopSpace; :: thesis: ( PT is metrizable implies PT is paracompact )
assume PT is metrizable ; :: thesis: PT is paracompact
then for FX being Subset-Family of st FX is Cover of & FX is open holds
ex GX being Subset-Family of st
( GX is open & GX is Cover of & GX is_finer_than FX & GX is locally_finite ) by Th12;
hence PT is paracompact by PCOMPS_1:def 4; :: thesis: verum