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 PT st FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) by Th6;
hence PT is paracompact by PCOMPS_1:def 3; :: thesis: verum