for X being non empty TopSpace
for A being Subset of X st A is open & A is dense holds
A is everywhere_dense by TOPS_1:23;