take PT = 1TopSp {1}; :: thesis: PT is paracompact
let FX be Subset-Family of PT; :: according to PCOMPS_1:def 3 :: thesis: ( FX is Cover of PT & FX is open implies 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 ) )
assume that
A1: FX is Cover of PT and
FX is open ; :: thesis: 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 )
consider GX being Subset-Family of PT such that
A2: ( GX c= FX & GX is Cover of PT ) and
GX is finite by A1;
take GX ; :: thesis: ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite )
thus ( GX is open & GX is Cover of PT & GX is_finer_than FX & GX is locally_finite ) by A2, Th10, SETFAM_1:12, TOPS_2:11; :: thesis: verum