let T be non empty TopSpace; :: thesis:
assume A1: T is compact ; :: thesis:
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 )

let FX be Subset-Family of T; :: thesis:
assume that
A2: FX is Cover of T and
A3: FX is open ; :: thesis:
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:
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:
thus GX is Cover of T by A5; :: thesis:
thus GX is_finer_than FX by A4, SETFAM_1:12; :: thesis:
thus GX is locally_finite by A6, Th10; :: thesis:

end;

hence T is paracompact ; :: thesis: