for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )