take PT = 1TopSp {1}; :: thesis: PT is paracompact
let FX be Subset-Family of ; :: according to PCOMPS_1:def 4 :: thesis: ( FX is Cover of & FX is open implies ex GX being Subset-Family of st
( GX is open & GX is Cover of & GX is_finer_than FX & GX is locally_finite ) )
assume that
A1: FX is Cover of and
A2: FX is open ; :: thesis: ex GX being Subset-Family of st
( GX is open & GX is Cover of & GX is_finer_than FX & GX is locally_finite )
consider GX being Subset-Family of such that
A3: ( GX c= FX & GX is Cover of ) and
GX is finite by A1;
take GX ; :: thesis: ( GX is open & GX is Cover of & GX is_finer_than FX & GX is locally_finite )
thus ( GX is open & GX is Cover of & GX is_finer_than FX & GX is locally_finite ) by A2, A3, Th13, SETFAM_1:17, TOPS_2:18; :: thesis: verum