for PT being non empty TopSpace st PT is metrizable holds
for FX being Subset-Family of PT st 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 & GX is_finer_than FX & GX is locally_finite )