take PT = 1TopSp {1}; :: thesis: PT is paracompact
let FX be Subset-Family of PT; :: according to PCOMPS_1:def 4 :: 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
A2: 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
A3: ( 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 A3, Th13, SETFAM_1:17, TOPS_2:18; :: thesis: verum