for T being TopStruct
for X being Subset of T st X is open holds
for B being finite Subset-Family of T st B is Basis of T holds
for Y being set holds
( not Y in Components B or X misses Y or Y c= X )