:: deftheorem defines paracompact PCOMPS_1:def 3 :
for IT being TopStruct holds
( IT is paracompact iff for FX being Subset-Family of IT st FX is Cover of IT & FX is open holds
ex GX being Subset-Family of IT st
( GX is open & GX is Cover of IT & GX is_finer_than FX & GX is locally_finite ) );