for T being non empty TopSpace st T is locally-compact holds
for D being countable Subset-Family of T st not D is empty & D is dense & D is open holds
for O being non empty Subset of T st O is open holds
ex A being irreducible Subset of T st
for V being Subset of T st V in D holds
A /\ O meets V