for PT being non empty TopSpace st PT is regular holds
for FX being Subset-Family of PT st FX is Cover of PT & FX is open holds
ex HX being Subset-Family of PT st
( HX is open & HX is Cover of PT & ( for V being Subset of PT st V in HX holds
ex W being Subset of PT st
( W in FX & Cl V c= W ) ) )