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 A2: ( FX is Cover of T & 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 )
then consider GX being Subset-Family of T such that
A3: ( GX c= FX & GX is Cover of T & GX is finite ) by A1, COMPTS_1:def 3;
take GX ; :: thesis: ( GX is open & GX is Cover of T & GX is_finer_than FX & GX is locally_finite )
thus GX is open :: thesis: ( GX is Cover of T & GX is_finer_than FX & GX is locally_finite )

proof

for W being Subset of T st W in GX holds
W is open by A2, A3, TOPS_2:def 1;
hence GX is open by TOPS_2:def 1; :: thesis: verum

end;

thus GX is Cover of T by A3; :: thesis: ( GX is_finer_than FX & GX is locally_finite )
thus GX is_finer_than FX by A3, SETFAM_1:17; :: thesis: GX is locally_finite
thus GX is locally_finite by A3, Th13; :: thesis: verum

end;

hence T is paracompact by Def4; :: thesis: verum