for PT being non empty TopSpace
for FX being Subset-Family of PT st PT is T_2 & PT is paracompact & FX is Cover of PT & FX is open holds
ex GX being Subset-Family of PT st
( GX is open & GX is Cover of PT & clf GX is_finer_than FX & GX is locally_finite )