let T be non empty TopSpace; :: thesis: ( T is compact implies T is paracompact )
assume A1: T is compact ; :: thesis: T is paracompact
for FX being Subset-Family of T st FX is Cover of T & FX is open holds
ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )

proof

let FX be Subset-Family of T; :: thesis: ( FX is Cover of T & FX is open implies ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite ) )
assume that
A2: FX is Cover of T and
A3: FX is open ; :: thesis: ex GX being Subset-Family of T st
( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of T such that
A4: GX c= FX and
A5: GX is Cover of T and
A6: GX is finite by A1, A2, A3;
take GX ; :: thesis: ( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
for W being Subset of T st W in GX holds
W is open by A3, A4, TOPS_2:def 1;
hence GX is open by TOPS_2:def 1; :: thesis: ( GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
thus GX is Cover of T by A5; :: thesis: ( GX is_finer_than FX & GX is locally_finite )
thus GX is_finer_than FX by A4, SETFAM_1:12; :: thesis: GX is locally_finite
thus GX is locally_finite by A6, Th10; :: thesis: verum

end;

hence T is paracompact ; :: thesis: verum